lean_rs_abi/
lib.rs

1//! Link-free Lean 4 ABI and toolchain metadata.
2//!
3//! This crate owns the static metadata that both build tooling and raw FFI
4//! bindings need: the supported Lean toolchain window, the required Lean
5//! runtime symbol names, and the `lean.h` layout constants. It is purely
6//! static — no build script, no `extern "C"` items, no link directives, and no
7//! probe of an installed toolchain — so any crate can depend on it without a
8//! Lean toolchain present. Live toolchain identity (installed version, header
9//! path, header digest) belongs to `lean-toolchain`, the crate whose job is
10//! toolchain discovery.
11
12#![forbid(unsafe_code)]
13
14pub mod consts;
15pub mod supported;
16
17mod symbols;
18
19pub use consts::{
20    LEAN_ARRAY, LEAN_CLOSURE, LEAN_CLOSURE_MAX_ARGS, LEAN_EXTERNAL, LEAN_MAX_CTOR_FIELDS, LEAN_MAX_CTOR_SCALARS_SIZE,
21    LEAN_MAX_CTOR_TAG, LEAN_MAX_SMALL_OBJECT_SIZE, LEAN_MPZ, LEAN_OBJECT_SIZE_DELTA, LEAN_PROMISE, LEAN_REF,
22    LEAN_RESERVED, LEAN_SCALAR_ARRAY, LEAN_STRING, LEAN_STRUCT_ARRAY, LEAN_TASK, LEAN_THUNK,
23};
24pub use supported::{
25    SUPPORTED_TOOLCHAINS, SupportedToolchain, supported_by_digest, supported_for, symbol_present_in_window,
26};
27pub use symbols::REQUIRED_SYMBOLS;
28
29/// Version of the `lean-rs-abi` crate, matching `Cargo.toml`.
30pub const VERSION: &str = env!("CARGO_PKG_VERSION");
31
32/// Return `true` iff `symbol` is required and present across the window.
33///
34/// More precisely: `symbol` is one of [`REQUIRED_SYMBOLS`] and no entry in
35/// [`SUPPORTED_TOOLCHAINS`] lists it under `missing_symbols`.
36#[must_use]
37pub fn symbol_in_all(symbol: &str) -> bool {
38    REQUIRED_SYMBOLS.contains(&symbol) && symbol_present_in_window(symbol)
39}
40
41#[cfg(test)]
42mod tests {
43    use super::{REQUIRED_SYMBOLS, VERSION, symbol_in_all};
44
45    #[test]
46    fn version_constant_matches_package() {
47        assert_eq!(VERSION, env!("CARGO_PKG_VERSION"));
48    }
49
50    #[test]
51    fn required_symbols_are_nonempty() {
52        assert!(!REQUIRED_SYMBOLS.is_empty());
53    }
54
55    #[test]
56    fn required_symbols_are_present_across_the_window() {
57        for &symbol in REQUIRED_SYMBOLS {
58            assert!(
59                symbol_in_all(symbol),
60                "{symbol} is not marked present in every supported toolchain",
61            );
62        }
63    }
64}
lean_rs_abi/lib.rs

lean_rs_abi/
lib.rs
