Struct LeanBuiltCapability 

pub struct LeanBuiltCapability { /* private fields */ }

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

Implementations

impl LeanBuiltCapability

pub fn path(path: impl Into<PathBuf>) -> Self

Build a descriptor from an embedded dylib path.

This remains supported for simple or compatibility cases. Prefer Self::manifest_path for shipped binaries because the manifest also carries dependency and loader-order facts:

let spec = lean_rs::LeanBuiltCapability::path(env!("LEAN_RS_CAPABILITY_MY_CAPABILITY_DYLIB"))
    .package("my_app")
    .module("MyCapability");

pub fn env(env_var: impl Into<String>) -> Self

Build a descriptor that resolves the dylib path from a runtime environment variable.

Prefer Self::path with Rust’s env! macro for redistributable binaries. Runtime environment lookup is useful for tests, local overrides, and launcher-managed deployments.

pub fn manifest_path(path: impl Into<PathBuf>) -> Self

Build a descriptor from an embedded artifact manifest path.

This is the canonical form for shipped binaries using CargoLeanCapability’s manifest output:

let spec = lean_rs::LeanBuiltCapability::manifest_path(
    env!("LEAN_RS_CAPABILITY_MY_CAPABILITY_MANIFEST"),
);

pub fn manifest_env(env_var: impl Into<String>) -> Self

Build a descriptor that resolves the artifact manifest path from a runtime environment variable.

Prefer Self::manifest_path with Rust’s env! macro for redistributable binaries. Runtime environment lookup is useful for tests, local overrides, and launcher-managed deployments.

pub fn env_var(self, env_var: impl Into<String>) -> Self

Preserve the Cargo environment variable name for diagnostics.

pub fn manifest_env_var(self, env_var: impl Into<String>) -> Self

Preserve the Cargo manifest environment variable name for diagnostics.

pub fn package(self, package: impl Into<String>) -> Self

Set the Lake package name used by the Lean initializer.

pub fn module(self, module: impl Into<String>) -> Self

Set the root Lean module name initialized by Rust.

pub fn dependency(self, dependency: LeanLibraryDependency) -> Self

Add a dependent Lean dylib that must stay alive with this capability.

This is primarily a bridge until lean-toolchain emits artifact manifests. Manifest-backed opening will feed the same dependency descriptors into the bundle loader.

pub fn dependencies( self, dependencies: impl IntoIterator<Item = LeanLibraryDependency>, ) -> Self

Add multiple dependent Lean dylibs that must stay alive with this capability.

pub fn package_name(&self) -> Option<&str>

Return the configured package name.

pub fn module_name(&self) -> Option<&str>

Return the configured module name.

pub fn dependency_descriptors(&self) -> &[LeanLibraryDependency]

Dependency dylibs that will be opened before the primary capability.

pub fn dylib_path(&self) -> LeanResult<PathBuf>

Resolve the capability dylib path.

Errors

Returns a host module-initialization error if neither a path nor a readable environment variable is configured.

pub fn resolved_manifest_path(&self) -> LeanResult<PathBuf>

Resolve the build artifact manifest path.

Errors

Returns a host module-initialization error if neither a path nor a readable manifest environment variable is configured.

Trait Implementations

impl Clone for LeanBuiltCapability

fn clone(&self) -> LeanBuiltCapability

Returns a duplicate of the value.

fn clone_from(&mut self, source: &Self)

Performs copy-assignment from source.

impl Debug for LeanBuiltCapability

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

Formats the value using the given formatter.

impl From<&BuiltLeanCapability> for LeanBuiltCapability

fn from(value: &BuiltLeanCapability) -> Self

Converts to this type from the input type.

impl PartialEq for LeanBuiltCapability

fn eq(&self, other: &LeanBuiltCapability) -> bool

Tests for self and other values to be equal, and is used by ==.

fn ne(&self, other: &Rhs) -> bool

Tests for !=. The default implementation is almost always sufficient, and should not be overridden without very good reason.

impl Eq for LeanBuiltCapability

impl StructuralPartialEq for LeanBuiltCapability