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 nat_int;
47pub mod object;
48pub mod refcount;
49pub mod scalar;
50pub mod string;
51pub mod supported;
52pub mod types;
53
54pub(crate) mod repr;
55
56pub use consts::{LEAN_HEADER_DIGEST, LEAN_HEADER_PATH, LEAN_RESOLVED_VERSION, LEAN_VERSION};
57pub use supported::{
58    SUPPORTED_TOOLCHAINS, SupportedToolchain, supported_by_digest, supported_for, symbol_present_in_window,
59};
60pub use types::{b_lean_obj_arg, b_lean_obj_res, lean_obj_arg, lean_obj_res, lean_object, u_lean_obj_arg};
61
62/// Return `true` iff `symbol` is required and present across the window.
63///
64/// More precisely: `symbol` is one of the names in [`REQUIRED_SYMBOLS`]
65/// **and** no entry in [`SUPPORTED_TOOLCHAINS`] lists it under
66/// `missing_symbols`. The thin convenience over
67/// [`symbol_present_in_window`] that adds the [`REQUIRED_SYMBOLS`]
68/// membership check.
69#[must_use]
70pub fn symbol_in_all(symbol: &str) -> bool {
71    REQUIRED_SYMBOLS.contains(&symbol) && symbol_present_in_window(symbol)
72}
73
74/// Names of `LEAN_EXPORT`'d symbols this crate's `extern "C"` blocks declare.
75///
76/// The `extern` blocks remain authoritative; tooling (`tests/linkage.rs`,
77/// `lean-toolchain`'s re-export, version-compatibility docs) reads this list
78/// to iterate over the surface without parsing source.
79pub const REQUIRED_SYMBOLS: &[&str] = &[
80    // init / runtime
81    "lean_initialize",
82    "lean_initialize_runtime_module",
83    "lean_initialize_thread",
84    "lean_finalize_thread",
85    "lean_setup_args",
86    "lean_init_task_manager",
87    "lean_init_task_manager_using",
88    "lean_finalize_task_manager",
89    // refcount + marking
90    "lean_dec_ref_cold",
91    "lean_mark_mt",
92    "lean_mark_persistent",
93    // object / allocators
94    "lean_alloc_object",
95    "lean_free_object",
96    "lean_object_byte_size",
97    "lean_object_data_byte_size",
98    // arrays
99    "lean_array_mk",
100    "lean_array_push",
101    "lean_array_to_list",
102    "lean_array_get_panic",
103    "lean_array_set_panic",
104    // strings
105    "lean_mk_string",
106    "lean_mk_string_unchecked",
107    "lean_mk_string_from_bytes",
108    "lean_mk_string_from_bytes_unchecked",
109    "lean_mk_ascii_string_unchecked",
110    "lean_string_push",
111    "lean_string_append",
112    "lean_string_mk",
113    "lean_string_data",
114    "lean_string_utf8_get",
115    "lean_string_utf8_next",
116    "lean_string_utf8_prev",
117    "lean_string_utf8_set",
118    "lean_string_utf8_extract",
119    "lean_string_eq_cold",
120    "lean_string_lt",
121    "lean_string_hash",
122    "lean_utf8_strlen",
123    "lean_utf8_n_strlen",
124    // Nat bignum dispatch
125    "lean_nat_big_succ",
126    "lean_nat_big_add",
127    "lean_nat_big_sub",
128    "lean_nat_big_mul",
129    "lean_nat_big_div",
130    "lean_nat_big_mod",
131    "lean_nat_big_eq",
132    "lean_nat_big_le",
133    "lean_nat_big_lt",
134    "lean_nat_overflow_mul",
135    // Int bignum dispatch
136    "lean_int_big_neg",
137    "lean_int_big_add",
138    "lean_int_big_sub",
139    "lean_int_big_mul",
140    "lean_int_big_div",
141    "lean_int_big_mod",
142    "lean_int_big_eq",
143    "lean_int_big_le",
144    "lean_int_big_lt",
145    "lean_int_big_nonneg",
146    // scalar widening
147    "lean_big_usize_to_nat",
148    "lean_big_uint64_to_nat",
149    "lean_cstr_to_nat",
150    "lean_big_int_to_int",
151    "lean_big_size_t_to_int",
152    "lean_big_int64_to_int",
153    "lean_cstr_to_int",
154    "lean_uint8_of_big_nat",
155    // closure dispatch
156    "lean_apply_1",
157    "lean_apply_2",
158    "lean_apply_3",
159    "lean_apply_4",
160    "lean_apply_5",
161    "lean_apply_6",
162    "lean_apply_7",
163    "lean_apply_8",
164    "lean_apply_9",
165    "lean_apply_10",
166    "lean_apply_11",
167    "lean_apply_12",
168    "lean_apply_13",
169    "lean_apply_14",
170    "lean_apply_15",
171    "lean_apply_16",
172    "lean_apply_n",
173    "lean_apply_m",
174    // IO
175    "lean_io_mark_end_initialization",
176    // external
177    "lean_register_external_class",
178];
lean_rs_sys/lib.rs

lean_rs_sys/
lib.rs
