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>) -> LeanBuiltCapability

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_toolchain::LeanBuiltCapability::path(env!("LEAN_RS_CAPABILITY_MY_CAPABILITY_DYLIB"))
    .package("my_app")
    .module("MyCapability");

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

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>) -> LeanBuiltCapability

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_toolchain::LeanBuiltCapability::manifest_path(
    env!("LEAN_RS_CAPABILITY_MY_CAPABILITY_MANIFEST"),
);

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

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>) -> LeanBuiltCapability

Preserve the Cargo environment variable name for diagnostics.

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

Preserve the Cargo manifest environment variable name for diagnostics.

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

Set the Lake package name used by the Lean initializer.

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

Set the root Lean module name initialized by Rust.

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

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

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

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 take_package_name(&mut self) -> Option<String>

Take the configured package name, leaving None behind.

pub fn take_module_name(&mut self) -> Option<String>

Take the configured module name, leaving None behind.

pub fn take_dependencies(&mut self) -> Vec<LeanLibraryDependency>

Take the recorded dependency descriptors, leaving an empty list.

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

Dependency dylibs that will be opened before the primary capability.

pub fn dylib_path(&self) -> Result<PathBuf, LeanBuiltCapabilityError>

Resolve the capability dylib path.

Errors

Returns LeanBuiltCapabilityError::MissingDylibSource if no dylib path or environment variable is configured, or LeanBuiltCapabilityError::EnvVarNotSet if the configured environment variable is not present at runtime.

pub fn resolved_manifest_path( &self, ) -> Result<PathBuf, LeanBuiltCapabilityError>

Resolve the build artifact manifest path.

Errors

Returns LeanBuiltCapabilityError::MissingManifestSource if no manifest path or manifest environment variable is configured, or LeanBuiltCapabilityError::EnvVarNotSet if the configured environment variable is not present at runtime.

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<(), Error>

Formats the value using the given formatter.

impl Eq for LeanBuiltCapability

impl From<&BuiltLeanCapability> for LeanBuiltCapability

fn from(value: &BuiltLeanCapability) -> LeanBuiltCapability

Converts to this type from the input type.

impl PartialEq for LeanBuiltCapability

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

Equality operator ==.

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

Inequality operator !=.

impl StructuralPartialEq for LeanBuiltCapability