Crate lean_rs_sys 

Raw FFI bindings for the Lean 4 C ABI.

Calling any function in this crate is unsafe. Prefer the safe front door in lean-rs — specifically its host, module, and error modules — for almost all use cases. Raw FFI is the escape hatch for embedders who need it.

Raw functions inherit Lean’s C ABI ownership rules:

• lean_obj_arg is owned (caller transfers a refcount).
• b_lean_obj_arg is borrowed (caller retains the refcount).
• lean_obj_res returns an owned reference.

lean_object is intentionally opaque: it is zero-sized and !Send + !Sync + !Unpin. Downstream code reaches refcount, tag, and payload state only through this crate’s pub unsafe fn helpers, never by reading fields. The crate’s layout assumptions are pinned at build time: build.rs computes the SHA-256 of the active toolchain’s include/lean/lean.h and requires it to match one entry in SUPPORTED_TOOLCHAINS. The matched entry’s first versions field is then exposed at runtime via consts::LEAN_RESOLVED_VERSION.

Layering:

• Inline mirrors of lean.h’s static inline helpers live alongside the extern "C" declarations for the matching category (e.g. refcount, string, array). Each pub unsafe fn carries a # Safety section, each unsafe { ... } block carries a // SAFETY: comment.
• A crate-private repr module defines the Lean object layout (LeanObjectRepr and friends). These types are intentionally not re-exported.

See crates/lean-rs-sys/README.md for the supported Lean version window and docs/bump-toolchain.md for the procedure to extend it.

Re-exports

pub use consts::LEAN_HEADER_DIGEST;

pub use consts::LEAN_HEADER_PATH;

pub use consts::LEAN_RESOLVED_VERSION;

pub use consts::LEAN_VERSION;

pub use supported::SUPPORTED_TOOLCHAINS;

pub use supported::SupportedToolchain;

pub use supported::supported_by_digest;

pub use supported::supported_for;

pub use supported::symbol_present_in_window;

pub use types::b_lean_obj_arg;

pub use types::b_lean_obj_res;

pub use types::lean_obj_arg;

pub use types::lean_obj_res;

pub use types::lean_object;

pub use types::u_lean_obj_arg;

Modules

array

Object and scalar arrays — externs and inline accessors from lean.h:815–1028.

closure

Closure objects — externs and inline accessors from lean.h:762–813.

consts

Compile-time constants resolved by build.rs (version + header digest) plus the tag enum from lean.h:83–95.

ctor

Constructor objects and polymorphic boxing — Rust mirrors of lean.h:642–760 and the lean_box_uint* / lean_box_float family at lean.h:2811–2873.

external

External objects — externs and inline accessors from lean.h:295–1332.

init

Runtime initialization and thread attachment.

io

IO-result helpers — mirrors lean.h:2893–2907.

nat_int

Bignum dispatch — externs from lean.h:1334–1853 plus the small-int ceiling constants.

object

Object inspection and allocation helpers — mirrors lean.h:312–630.

refcount

Refcount fast paths — Rust mirrors of lean.h:536–563.

scalar

Boxed-scalar conversions — Rust mirrors of lean.h:1356–2065.

string

String objects — externs and inline accessors from lean.h:1157–1234.

supported

The supported Lean toolchain window.

types

Opaque lean_object plus the calling-convention typedefs from lean.h:131–168.

Constants

REQUIRED_SYMBOLS

Names of LEAN_EXPORT’d symbols this crate’s extern "C" blocks declare.

Functions

symbol_in_all

Return true iff symbol is required and present across the window.