Please check the build logs for more information.
See Builds for ideas on how to fix a failed build, or Metadata for how to configure docs.rs builds.
If you believe this is docs.rs' fault, open an issue.
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.
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
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 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:
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 or MIT license, at your option.