lean-rs 0.1.2

Safe Rust bindings for Lean 4 interop: runtime initialization, object handles, typed ABI conversions, module loading, exported function calls, semantic handles, and callback handles.
Documentation 
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62

//! Loading and initializing compiled Lean modules.
//!
//! The normal shipped-capability path is [`LeanCapability`], which stores a
//! [`LeanLibraryBundle`] internally. The lower-level surface has three RAII
//! types:
//!
//! - [`LeanLibrary`] — a Lake-built native shared object opened through
//!   the platform dynamic loader.
//! - [`LeanLibraryBundle`] — a primary shared object plus dependent Lean
//!   dylibs anchored for the same lifetime.
//! - [`LeanModule`] — proof that a named Lean module hosted by a
//!   [`LeanLibrary`] has been initialized to `IO.ok(())`.
//! - [`LeanCapabilityPreflight`] — manifest and artifact checks that turn
//!   package/loader failures into stable repair hints before opening.
//!
//! Construction of either type requires a [`crate::LeanRuntime`]
//! borrow, so use-before-init is structurally impossible. The
//! `'lean` lifetime cascade keeps every derived handle bound to the
//! runtime witness; the secondary `'lib` lifetime on [`LeanModule`]
//! keeps initialized modules from outliving the dylib that hosts them.
//!
//! ```ignore
//! let runtime = lean_rs::LeanRuntime::init()?;
//! let library = lean_rs::module::LeanLibrary::open(runtime, "path/to/libfoo.dylib")?;
//! let module  = library.initialize_module("foo_pkg", "Foo.Bar")?;
//! ```
//!
//! Callers do not name raw initializer symbols, choose the Lean
//! `builtin` flag, decode `IO` results, or maintain idempotency state;
//! all of that lives in the `pub(crate) module::initializer`
//! infrastructure. Typed exported-function handles cross the public
//! boundary as [`LeanExported`] and [`LeanIo`]; see `exported` for
//! the call shape.

pub(crate) mod bundle;
pub(crate) mod capability;
pub(crate) mod exported;
pub(crate) mod initializer;
pub(crate) mod library;
pub(crate) mod loaded;
pub(crate) mod preflight;

pub use bundle::{LeanLibraryBundle, LeanLibraryDependency, LeanModuleInitializer};
pub use capability::{LeanBuiltCapability, LeanCapability};
pub use exported::{DecodeCallResult, LeanArgs, LeanExported, LeanIo};
pub use library::LeanLibrary;
pub use loaded::LeanModule;
pub use preflight::{
    LeanCapabilityPreflight, LeanLoaderCheck, LeanLoaderDiagnosticCode, LeanLoaderReport, LeanLoaderSeverity,
};

// `LeanAbi` lives in `crate::abi::traits` but appears in the public
// signature of [`LeanModule::exported`] (as a per-arg bound) and in the
// docstrings for [`LeanExported`]/[`LeanIo`]. Re-export it at the
// `module` boundary so rustdoc resolves intra-crate links and so a
// downstream crate that wants to inspect the bound has a single import
// path. The trait remains sealed; the re-export only widens the doc
// surface, not the impl surface.
pub use crate::abi::traits::LeanAbi;

#[cfg(test)]
mod tests;