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

ABI constants for lean-rs-sys.

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.

memory

Runtime memory guardrail entry points.

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

Compatibility re-exports for the supported Lean toolchain window.

types

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

Structs

SupportedToolchain

One ABI-equivalence class in the supported toolchain window.

Constants

REQUIRED_SYMBOLS

SUPPORTED_TOOLCHAINS

The supported Lean toolchain window.

Functions

supported_by_digest

Return the SupportedToolchain entry whose header_digest matches the given lowercase-hex SHA-256 string, if any.

supported_for

Return the SupportedToolchain entry that includes version, if any.

symbol_in_all

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

symbol_present_in_window

Return true iff no SupportedToolchain entry lists symbol under missing_symbols. Combine with crate::REQUIRED_SYMBOLS for a membership check via crate::symbol_in_all.