lean-toolchain 0.1.2

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
59
60
61
62
63
64
65

# 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.