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 build helpers and the lean-rs safe front door) ultimately threads through this crate.

Lean's header layout is not part of this crate's public semver. The semver promise covers the opaque public types, the pub unsafe fn surface, and the SUPPORTED_TOOLCHAINS table. The LeanObjectRepr layout struct is pub(crate) and may be updated to track Lean version bumps without breaking downstream code that uses the pub unsafe fn helpers.

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

Currently 4.26.0 through 4.29.1 plus the 4.30.0-rc2 release candidate; the authoritative list lives in crates/lean-rs-sys/src/supported.rs. The build script computes a SHA-256 digest over the discovered lean.h and accepts any digest matching an entry in the SUPPORTED_TOOLCHAINS 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 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.

Bumping the window is the bump procedure: 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_SYSROOT 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. The metadata-only feature is for crates such as lean-toolchain that need the supported-window metadata from build scripts without linking the build-script binary to libleanshared. See build.rs for details.

When DOCS_RS=1, the build script emits documentation-only metadata for the latest supported Lean window entry and deliberately skips Lean discovery and link directives. docs.rs does not install Lean, so published API docs must not require a local toolchain.

License

Dual-licensed under either of Apache License, Version 2.0 or MIT license, at your option.