Struct CargoLeanCapability 

pub struct CargoLeanCapability { /* private fields */ }

Build-script helper for shipping a Rust crate with bundled Lean code.

This is the canonical downstream build.rs entry point. It composes emit_lean_link_directives_checked, build_lake_target, and the cargo:rustc-env=... directives that carry a JSON artifact manifest and a backward-compatible dylib path into Rust code at compile time.

fn main() -> Result<(), Box<dyn std::error::Error>> {
    lean_toolchain::CargoLeanCapability::new("lean", "MyCapability")
        .package("my_app")
        .module("MyCapability")
        .build()?;
    Ok(())
}

Implementations

impl CargoLeanCapability

pub fn new( project_root: impl Into<PathBuf>, target_name: impl Into<String>, ) -> Self

Create a build helper for a Lake project and lean_lib target.

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

Set the Lake package name used by the module initializer.

If omitted, the helper infers the package from lake-manifest.json or the project’s lakefile (lakefile.lean or lakefile.toml), matching build_lake_target.

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

Set the root Lean module name initialized by Rust.

Defaults to the Lake target name.

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

Override the generated Cargo environment variable name.

The default is LEAN_RS_CAPABILITY_<TARGET>_DYLIB, with the target converted to screaming snake case.

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

Override the generated Cargo environment variable name for the artifact manifest.

The default is LEAN_RS_CAPABILITY_<TARGET>_MANIFEST, with the target converted to screaming snake case.

pub fn lean_sysroot(self, sysroot: impl Into<PathBuf>) -> Self

Build and link against a specific Lean sysroot.

sysroot is the Lean prefix containing include/lean/lean.h and, for real Lake builds, bin/lake. Self::build uses this sysroot for link-directive discovery. Both Self::build and Self::build_quiet pass it only to the spawned Lake command as LEAN_SYSROOT and run <sysroot>/bin/lake; they do not mutate the parent process environment.

pub fn lean_num_threads(self, threads: u32) -> Self

Cap the parallelism of the spawned lake build by setting LEAN_NUM_THREADS.

Lake 5.x has no --jobs flag; it derives both the number of concurrent build jobs and each spawned lean’s task-manager thread count from LEAN_NUM_THREADS. Leaving this unset uses Lake’s hardware-concurrency default, which fans out to one multi-GB lean process per core and can exhaust memory on large machines. Both Self::build and Self::build_quiet pass this only to the spawned Lake command; they do not mutate the parent process environment.

pub fn export_signature(self, signature: LeanExportSignature) -> Self

Add trusted ABI metadata for one exported Lean symbol.

The runtime checked-lookup API accepts a Rust call shape only when it exactly matches one of these manifest entries.

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

Add a dependent Lean dylib that must be loaded before this capability.

Use this when the capability imports another shipped Lake package whose shared library was built separately. The dependency is recorded in the same artifact manifest consumed by lean-rs and the worker parent, so callers do not need to edit manifest JSON after the build.

pub fn build(self) -> Result<BuiltLeanCapability, LinkDiagnostics>

Emit link directives, build the Lake shared library, write the artifact manifest, and emit cargo:rustc-env directives for the manifest and compatibility dylib path.

Errors

Returns LinkDiagnostics if Lean cannot be discovered, Lake cannot build the target, or the target output cannot be resolved.

pub fn build_quiet(self) -> Result<BuiltLeanCapability, LinkDiagnostics>

Same as Self::build without printing Cargo directives.

This exists for tests and internal callers. Downstream build.rs scripts should use Self::build.

Errors

Returns LinkDiagnostics if Lake cannot build the target or the target output cannot be resolved.

Trait Implementations

impl Clone for CargoLeanCapability

fn clone(&self) -> CargoLeanCapability

Returns a duplicate of the value.

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

Performs copy-assignment from source.

impl Debug for CargoLeanCapability

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

Formats the value using the given formatter.