# lean-rs-sys
Raw FFI bindings for the Lean 4 C ABI. Sits at the bottom of the `lean-rs` workspace; everything above it (the
[`lean-toolchain`](../lean-toolchain/) build helpers and the [`lean-rs`](../lean-rs/) safe front door) ultimately
threads through this crate.
**Calling any function in this crate is `unsafe`.** Public types are opaque (`lean_object` is `[u8; 0]` plus phantom
markers, `!Send + !Sync + !Unpin`); downstream code reaches refcount, tag, and payload state only through
`pub unsafe fn` helpers, each of which carries a `# Safety` section naming the invariant the caller must uphold. Prefer
the safe layers in `lean-rs` for almost every use case; reach for this crate only when the safe surface is missing a
capability you need.
## Supported Lean window
`lean-rs-sys` supports a contiguous window of Lean 4 stable releases — currently **4.26.0 through
4.29.1** (see [`crates/lean-rs-sys/src/supported.rs`](https://github.com/jcreinhold/lean-rs/blob/main/crates/lean-rs-sys/src/supported.rs)
for the authoritative list). The build script computes a SHA-256 digest over the discovered
`lean.h` and accepts any digest that matches an entry in the
[`SUPPORTED_TOOLCHAINS`](https://github.com/jcreinhold/lean-rs/blob/main/crates/lean-rs-sys/src/supported.rs) table.
Releases that ship a byte-identical `lean.h` share one entry. A miss fails the build with a
bounded diagnostic naming the discovered digest and the full window.
The build script also emits `cargo:rustc-cfg=lean_v_X_Y_Z` for the matched entry's resolved
version, so downstream code can `#[cfg]`-gate per-version divergences. As of v0.1.0 no
divergence requires gating: layout structs are byte-identical and all 87 `REQUIRED_SYMBOLS`
entries are present across the entire window.
Lean's header layout is **not** part of this crate's public semver. The opaque types, the
`pub unsafe fn` surface, and the `SUPPORTED_TOOLCHAINS` table are.
Bumping the window is the [bump procedure](https://github.com/jcreinhold/lean-rs/blob/main/docs/bump-toolchain.md):
add a row to `SUPPORTED_TOOLCHAINS`, add a CI matrix entry, run the local sweep
(`scripts/test-all-toolchains.sh`), open a PR.
## Build environment
`build.rs` discovers Lean via `lean --print-prefix` (or `LEAN_PREFIX` when set), emits the appropriate
`cargo:rustc-link-*` directives, and exposes `LEAN_VERSION`, `LEAN_HEADER_PATH`, and `LEAN_HEADER_DIGEST` as build-time
environment variables consumed by `consts.rs`. The default features (`dynamic`, `mimalloc`) link against
`libleanshared`; the `static` feature is available but requires extending the link set beyond what `lean.h` alone
demands. See `build.rs` for the details.
## License
Dual-licensed under either of [Apache License, Version 2.0](../../LICENSE-APACHE) or
[MIT license](../../LICENSE-MIT), at your option.