Struct LeanLibrary 

pub struct LeanLibrary<'lean> { /* private fields */ }

A loaded native Lean shared object.

Wraps a libloading::Library and hands out initialized module handles via LeanLibrary::initialize_module. The 'lean lifetime parameter ties the library to the witnessing crate::LeanRuntime borrow; the resulting LeanModule handles borrow from self, so they cannot outlive the library that hosts them.

Neither Send nor Sync: the &'lean LeanRuntime field inherits the runtime’s per-thread restriction (LeanRuntime: !Sync implies &LeanRuntime: !Send, and &LeanRuntime: Sync iff LeanRuntime: Sync). A negative-bound compile-time assertion in the test module fails if either auto-trait is ever implemented.

Implementations

impl<'lean> LeanLibrary<'lean>

pub fn open( runtime: &'lean LeanRuntime, path: impl AsRef<Path>, ) -> LeanResult<Self>

Load a Lake-built Lean shared object from path.

Reads the file’s symbol table once to classify each exported symbol as a function (text/code section) or a Lean nullary-constant global (data/rodata/bss section). The classification is consulted by LeanModule::exported_unchecked so callers never write the function-vs-global distinction at the call site. The walk is cheap (a single std::fs::read plus an in-memory parse) and amortised across every later lookup.

The runtime borrow is the type-level proof that the Lean runtime is up; it is retained for the symbol-initialization step but otherwise unused. Module initialization happens later through LeanLibrary::initialize_module.

Errors

Returns LeanError::Host with stage HostStage::Load if:

• the file cannot be read (missing, permission denied),
• the bytes do not parse as a recognised object format (Mach-O, ELF, PE),
• the dynamic linker fails to open the file (missing transitive dependency, architecture mismatch, …).

The diagnostic embeds the path and the underlying error message.

pub fn open_globally( runtime: &'lean LeanRuntime, path: impl AsRef<Path>, ) -> LeanResult<Self>

Open a Lake-built Lean shared object with globally visible symbols (POSIX RTLD_GLOBAL on Unix; the Windows side stays on the default loader since DLL symbols are already global).

The same contract as LeanLibrary::open, plus: symbols defined by this dylib become visible to the dynamic linker’s global namespace, so any subsequently dlopened dylib whose initializer chain references them resolves correctly.

The motivating case is the lean-rs-host shim load: the host shim package imports the generic interop shim package, so opening the generic dylib globally first lets the host shim initializer resolve the generated LeanRsInterop.* references normally.

Errors

Same as LeanLibrary::open.

pub fn initialize_module<'lib>( &'lib self, package: &str, module: &str, ) -> LeanResult<LeanModule<'lean, 'lib>>

Initialize the Lean module identified by (package, module).

Resolves the Lake-mangled initializer symbol against this library, invokes it under a panic boundary with the runtime builtin flag, and decodes the resulting IO Unit. Idempotent: the Lean-emitted initializer body short-circuits to IO.ok(()) on its second and later calls, so repeated invocations are safe and cheap.

Errors

Returns LeanError::Host with:

• HostStage::Link if package or module is not a valid Lake identifier, or the mangled initializer symbol is not exported by this library.
• HostStage::Load if the initializer panics or returns IO.error.

Trait Implementations

impl Debug for LeanLibrary<'_>

fn fmt(&self, f: &mut Formatter<'_>) -> Result

Formats the value using the given formatter.