lean_rs_abi/consts.rs
1//! Static `lean.h` layout constants: object tag bytes, allocator ceilings, and
2//! constructor-shape limits.
3//!
4//! These are layout facts of the Lean C ABI, identical across the supported
5//! toolchain window, so they are plain literals with no build-time probe.
6//!
7//! Live toolchain identity (the installed version, header path, and header
8//! digest) is deliberately *not* here: resolving it requires probing an
9//! installed toolchain, which a link-free metadata crate must not do. It lives
10//! in `lean-toolchain` (`LEAN_VERSION`, `LEAN_HEADER_PATH`,
11//! `LEAN_HEADER_DIGEST`, `LEAN_RESOLVED_VERSION`), the crate whose job is
12//! toolchain discovery.
13
14// Tag constants—`lean.h:83–95`.
15pub const LEAN_MAX_CTOR_TAG: u8 = 243;
16pub const LEAN_PROMISE: u8 = 244;
17pub const LEAN_CLOSURE: u8 = 245;
18pub const LEAN_ARRAY: u8 = 246;
19pub const LEAN_STRUCT_ARRAY: u8 = 247;
20pub const LEAN_SCALAR_ARRAY: u8 = 248;
21pub const LEAN_STRING: u8 = 249;
22pub const LEAN_MPZ: u8 = 250;
23pub const LEAN_THUNK: u8 = 251;
24pub const LEAN_TASK: u8 = 252;
25pub const LEAN_REF: u8 = 253;
26pub const LEAN_EXTERNAL: u8 = 254;
27pub const LEAN_RESERVED: u8 = 255;
28
29// Object-allocator constants—`lean.h:30–32`.
30pub const LEAN_CLOSURE_MAX_ARGS: usize = 16;
31pub const LEAN_OBJECT_SIZE_DELTA: usize = 8;
32pub const LEAN_MAX_SMALL_OBJECT_SIZE: usize = 4096;
33
34// Constructor-shape ceilings—`lean.h:97–98`.
35pub const LEAN_MAX_CTOR_FIELDS: usize = 256;
36pub const LEAN_MAX_CTOR_SCALARS_SIZE: usize = 1024;