Struct LeanCapability 

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

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

Implementations

impl<'lean> LeanCapability<'lean>

pub fn from_build_manifest( runtime: &'lean LeanRuntime, spec: LeanBuiltCapability, ) -> LeanResult<Self>

Open and initialize a build-script produced Lean capability from its JSON artifact manifest.

Errors

Returns LeanError when the manifest path cannot be resolved, the manifest is missing, malformed, or unsupported, or the bundle described by the manifest cannot be opened.

pub fn from_build_env( runtime: &'lean LeanRuntime, spec: LeanBuiltCapability, ) -> LeanResult<Self>

Open and initialize a build-script produced Lean capability from a direct dylib path.

This compatibility path cannot carry dependency ordering by itself. Prefer Self::from_build_manifest for shipped crates.

Errors

Returns LeanError when the dylib path cannot be resolved, the dynamic loader cannot open it, or the configured module initializer fails.

pub fn open( runtime: &'lean LeanRuntime, dylib_path: impl AsRef<Path>, package: impl Into<String>, module: impl Into<String>, ) -> LeanResult<Self>

Open and initialize a capability from an explicit dylib path and initializer names.

Errors

Returns LeanError when the dynamic loader cannot open the dylib or the configured module initializer fails.

pub fn open_with_dependencies( runtime: &'lean LeanRuntime, dylib_path: impl AsRef<Path>, package: impl Into<String>, module: impl Into<String>, dependencies: impl IntoIterator<Item = LeanLibraryDependency>, ) -> LeanResult<Self>

Open and initialize a capability with explicitly described dependency dylibs.

This is the runtime form artifact manifests feed. Use LeanCapability::from_build_manifest for shipped crates when build-script metadata is available.

Errors

Returns LeanError when a dependency or primary dylib cannot be loaded, or when a dependency or primary module initializer fails.

pub fn module(&self) -> LeanResult<LeanModule<'lean, '_>>

Return an initialized module handle.

Lean module initializers are idempotent, so obtaining the handle after construction is cheap and safe.

Errors

Returns LeanError if the module initializer unexpectedly fails when invoked again.

pub fn library(&self) -> &LeanLibrary<'lean>

Borrow the underlying library for advanced symbol access.

pub fn bundle(&self) -> &LeanLibraryBundle<'lean>

Borrow the bundle that anchors this capability and its dependencies.

pub fn package_name(&self) -> &str

Lake package name used by the initializer.

pub fn module_name(&self) -> &str

Root Lean module name used by the initializer.