lean-toolchain

Lean 4 toolchain discovery, fingerprinting, link diagnostics, and build.rs helpers for the lean-rs project. Sits above lean-rs-sys (raw FFI + header digest + symbol allowlist) and below lean-rs.

Owns the typed ToolchainFingerprint, the Lake fixture digest, layered link diagnostics, and reusable build-script helpers downstream embedders can call from their own build.rs. Re-exports LEAN_VERSION, LEAN_HEADER_DIGEST, and REQUIRED_SYMBOLS from lean-rs-sys so the allowlist lives in one place.

It also owns Lake module discovery for higher layers. discover_lake_modules resolves a Lake root, discovers lean_lib source roots, validates module names, enumerates Lean source files deterministically, and returns source-set fingerprints. This discovery layer does not know worker pools or downstream cache policy; lean-rs-worker uses it to build import/session batches.

Runtime application code usually does not depend on this crate directly: it shows up transitively through lean-rs. Downstream crates that ship Lean source commonly depend on it from build.rs, where CargoLeanCapability builds the Lake shared library and emits the compile-time path that runtime code opens through lean-rs or lean-rs-worker. Same-process apps pair that path with LeanCapability; worker apps pair it with LeanWorkerChild and an app-owned worker-child binary. See docs/recipes/ship-crate-with-lean.md.

Quick start in a downstream build.rs

[build-dependencies]
lean-toolchain = "0.1"

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

CargoLeanCapability emits Lean link directives, Cargo rerun triggers, runs lake build <target>:shared, resolves the built dylib path, writes a JSON artifact manifest, and emits deterministic LEAN_RS_CAPABILITY_<TARGET>_MANIFEST plus compatibility LEAN_RS_CAPABILITY_<TARGET>_DYLIB compile-time environment variables. build_lake_target remains available as the lower-level escape hatch and also covers Lake targets that depend on the generic lean-rs-interop-shims package. It reports cache hits and misses on stderr, emits only cargo: directives on stdout, and returns typed LinkDiagnostics for missing lake, target lookup failures, Lake build failures, and unresolved outputs.

See docs/recipes/ship-crate-with-lean.md for the canonical shipped-crate layout.

See the workspace README for the five-crate architecture overview and docs/architecture/02-versioning-and-compatibility.md for the supported Lean window.

License

Dual-licensed under MIT or Apache-2.0 at your option.