lean_rs/module/
mod.rs

1//! Loading and initializing compiled Lean modules.
2//!
3//! The normal shipped-capability path is [`LeanCapability`], which stores a
4//! [`LeanLibraryBundle`] internally. The lower-level surface has three RAII
5//! types:
6//!
7//! - [`LeanLibrary`] — a Lake-built native shared object opened through
8//!   the platform dynamic loader.
9//! - [`LeanLibraryBundle`] — a primary shared object plus dependent Lean
10//!   dylibs anchored for the same lifetime.
11//! - [`LeanModule`] — proof that a named Lean module hosted by a
12//!   [`LeanLibrary`] has been initialized to `IO.ok(())`.
13//! - [`LeanCapabilityPreflight`] — manifest and artifact checks that turn
14//!   package/loader failures into stable repair hints before opening.
15//!
16//! Construction of either type requires a [`crate::LeanRuntime`]
17//! borrow, so use-before-init is structurally impossible. The
18//! `'lean` lifetime cascade keeps every derived handle bound to the
19//! runtime witness; the secondary `'lib` lifetime on [`LeanModule`]
20//! keeps initialized modules from outliving the dylib that hosts them.
21//!
22//! ```ignore
23//! let runtime = lean_rs::LeanRuntime::init()?;
24//! let library = lean_rs::module::LeanLibrary::open(runtime, "path/to/libfoo.dylib")?;
25//! let module  = library.initialize_module("foo_pkg", "Foo.Bar")?;
26//! ```
27//!
28//! Callers do not name raw initializer symbols, choose the Lean
29//! `builtin` flag, decode `IO` results, or maintain idempotency state;
30//! all of that lives in the `pub(crate) module::initializer`
31//! infrastructure. Typed exported-function handles cross the public
32//! boundary as [`LeanExported`] and [`LeanIo`]; see `exported` for
33//! the call shape.
34
35pub(crate) mod bundle;
36pub(crate) mod capability;
37pub(crate) mod exported;
38pub(crate) mod initializer;
39pub(crate) mod library;
40pub(crate) mod loaded;
41pub(crate) mod preflight;
42
43pub use bundle::{LeanLibraryBundle, LeanLibraryDependency, LeanModuleInitializer};
44pub use capability::{LeanBuiltCapability, LeanCapability};
45pub use exported::{DecodeCallResult, LeanArgs, LeanExported, LeanIo};
46pub use library::LeanLibrary;
47pub use loaded::LeanModule;
48pub use preflight::{
49    LeanCapabilityPreflight, LeanLoaderCheck, LeanLoaderDiagnosticCode, LeanLoaderReport, LeanLoaderSeverity,
50};
51
52// `LeanAbi` lives in `crate::abi::traits` but appears in the public
53// signature of [`LeanModule::exported`] (as a per-arg bound) and in the
54// docstrings for [`LeanExported`]/[`LeanIo`]. Re-export it at the
55// `module` boundary so rustdoc resolves intra-crate links and so a
56// downstream crate that wants to inspect the bound has a single import
57// path. The trait remains sealed; the re-export only widens the doc
58// surface, not the impl surface.
59pub use crate::abi::traits::LeanAbi;
60
61#[cfg(test)]
62mod tests;
lean_rs/module/mod.rs

lean_rs/module/
mod.rs
