Module module 

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.

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.

Re-exports

pub use crate::abi::traits::LeanAbi;

pub use crate::abi::traits::LeanCReprAbi;

Structs

LeanBuiltCapability

Runtime descriptor for a Lean capability built by a downstream build.rs.

LeanCapability

Opened Lean capability whose dylib path and initializer names came from the build-script pairing.

LeanExportArgAbi

ABI shape of one exported function argument.

LeanExportReturnAbi

ABI shape of an exported result.

LeanExportSignature

Trusted manifest signature for one Lean export.

LeanExported

A typed handle for an exported Lean symbol.

LeanIo

Return-type marker for Lean exports declared IO α.

LeanLibrary

A loaded native Lean shared object.

LeanLibraryBundle

A primary Lean capability plus its dependent Lean dylibs.

LeanLibraryDependency

Dependency dylib that must stay alive while a capability is loaded.

LeanLoaderCheck

One bounded preflight finding.

LeanLoaderReport

Structured result of loader preflight for one capability manifest.

LeanModule

A Lean module that has been linked and initialized successfully.

LeanModuleInitializer

Initializer for a Lean module hosted by a loaded dylib.

LeanRuntimePreflight

Runtime preflight runner for manifest-backed Lean capabilities.

Enums

BuiltCapabilityArtifact

Which artifact a LeanBuiltCapability resolution was looking for.

LeanBuiltCapabilityError

Errors returned when resolving a LeanBuiltCapability descriptor.

LeanCheckedExportError

Typed failure from manifest-backed checked export lookup.

LeanExportAbiRepr

C ABI representation for one exported argument or result slot.

LeanExportOwnership

Ownership convention for one ABI slot.

LeanExportResultConvention

How an exported result is decoded.

LeanExportSymbolKind

Whether an exported symbol is callable code or a Lean persistent global.

LeanLoaderDiagnosticCode

Stable preflight diagnostic codes for manifest-backed capability loading.

LeanLoaderSeverity

Severity of one loader preflight finding.

Traits

DecodeCallResult

How to decode an owned Lean call result into a Rust value.

LeanArgs

Per-arity marker for LeanExported’s argument tuple.

Type Aliases

LeanCapabilityPreflight

Backwards-compatible alias for LeanRuntimePreflight.