lean_rs_sys/
lib.rs

1//! Raw FFI bindings for the Lean 4 C ABI.
2//!
3//! **Calling any function in this crate is `unsafe`.** Prefer the safe front
4//! door in [`lean-rs`](https://docs.rs/lean-rs)—specifically its `host`,
5//! `module`, and `error` modules—for almost all use cases. Raw FFI is the
6//! escape hatch for embedders who need it.
7//!
8//! Raw functions inherit Lean's C ABI ownership rules:
9//! - `lean_obj_arg` is **owned** (caller transfers a refcount).
10//! - `b_lean_obj_arg` is **borrowed** (caller retains the refcount).
11//! - `lean_obj_res` returns an **owned** reference.
12//!
13//! [`lean_object`] is intentionally opaque: it is zero-sized and `!Send +
14//! !Sync + !Unpin`. Downstream code reaches refcount, tag, and payload state
15//! only through this crate's `pub unsafe fn` helpers, never by reading
16//! fields. The crate's layout assumptions are pinned at build time: `build.rs`
17//! computes the SHA-256 of the active toolchain's `include/lean/lean.h` and
18//! requires it to match one entry in [`SUPPORTED_TOOLCHAINS`]. The matched
19//! entry's first `versions` field is then exposed at runtime via
20//! [`consts::LEAN_RESOLVED_VERSION`].
21//!
22//! Layering:
23//! - Inline mirrors of `lean.h`'s `static inline` helpers live alongside the
24//!   `extern "C"` declarations for the matching category (e.g. refcount,
25//!   string, array). Each `pub unsafe fn` carries a `# Safety` section, each
26//!   `unsafe { ... }` block carries a `// SAFETY:` comment.
27//! - A crate-private `repr` module defines the Lean object layout
28//!   (`LeanObjectRepr` and friends). These types are intentionally not
29//!   re-exported.
30//!
31//! See `crates/lean-rs-sys/README.md` for the supported Lean version window
32//! and `docs/bump-toolchain.md` for the procedure to extend it.
33
34#![allow(unsafe_code)]
35#![allow(non_camel_case_types)]
36#![allow(non_snake_case)]
37#![allow(non_upper_case_globals)]
38
39pub mod array;
40pub mod closure;
41pub mod consts;
42pub mod ctor;
43pub mod external;
44pub mod init;
45pub mod io;
46pub mod memory;
47pub mod nat_int;
48pub mod object;
49pub mod refcount;
50pub mod scalar;
51pub mod string;
52pub mod supported;
53pub mod types;
54
55pub(crate) mod repr;
56
57pub use consts::{LEAN_HEADER_DIGEST, LEAN_HEADER_PATH, LEAN_RESOLVED_VERSION, LEAN_VERSION};
58pub use lean_rs_abi::{
59    REQUIRED_SYMBOLS, SUPPORTED_TOOLCHAINS, SupportedToolchain, supported_by_digest, supported_for, symbol_in_all,
60    symbol_present_in_window,
61};
62pub use types::{b_lean_obj_arg, b_lean_obj_res, lean_obj_arg, lean_obj_res, lean_object, u_lean_obj_arg};
lean_rs_sys/lib.rs

lean_rs_sys/
lib.rs
