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 lakefile.lean, 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 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.