lean-toolchain 0.1.3

Lean 4 toolchain discovery, fingerprinting, symbol allowlist, and build-script helpers reusable by downstream embedders' own build.rs scripts.
Documentation 
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58

# lean-toolchain

Lean 4 toolchain discovery, fingerprinting, link diagnostics, and `build.rs` helpers for the `lean-rs` project. Sits
above [`lean-rs-sys`](https://docs.rs/lean-rs-sys) (raw FFI + header digest + symbol allowlist) and below
[`lean-rs`](https://docs.rs/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`](https://github.com/jcreinhold/lean-rs/blob/main/docs/recipes/ship-crate-with-lean.md).

## Quick start in a downstream `build.rs`

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

```rust,ignore
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`](https://github.com/jcreinhold/lean-rs/blob/main/docs/recipes/ship-crate-with-lean.md)
for the canonical shipped-crate layout.

See the [workspace README](https://github.com/jcreinhold/lean-rs) for the five-crate architecture overview and
[`docs/architecture/02-versioning-and-compatibility.md`](https://github.com/jcreinhold/lean-rs/blob/main/docs/architecture/02-versioning-and-compatibility.md)
for the supported Lean window.

## License

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