lean_rs_sys/
consts.rs

1//! Compile-time constants resolved by `build.rs` (version + header digest)
2//! plus the tag enum from `lean.h:83–95`.
3
4/// `LEAN_VERSION_STRING` as read from the active toolchain's `version.h`
5/// (e.g. `"4.29.1"`).
6pub const LEAN_VERSION: &str = env!("LEAN_VERSION");
7
8/// Version string from the matched supported-toolchain entry.
9///
10/// The build script resolves this from the
11/// [`SupportedToolchain`](crate::SupportedToolchain) entry whose
12/// `header_digest` matched at build time. Equal to one of the `versions`
13/// entries in [`SUPPORTED_TOOLCHAINS`](crate::SUPPORTED_TOOLCHAINS); in
14/// practice equal to [`LEAN_VERSION`], but the build accepts any version
15/// whose `lean.h` digest matches a supported entry.
16pub const LEAN_RESOLVED_VERSION: &str = env!("LEAN_RESOLVED_VERSION");
17
18/// Filesystem path to the `lean.h` that the build was resolved against.
19pub const LEAN_HEADER_PATH: &str = env!("LEAN_HEADER_PATH");
20
21/// SHA-256 of the resolved `lean.h`. Computed by `build.rs` and equal to
22/// the `header_digest` of the matched
23/// [`SupportedToolchain`](crate::SupportedToolchain) entry.
24pub const LEAN_HEADER_DIGEST: &str = env!("LEAN_HEADER_DIGEST");
25
26// Tag constants — `lean.h:83–95`.
27pub const LEAN_MAX_CTOR_TAG: u8 = 243;
28pub const LEAN_PROMISE: u8 = 244;
29pub const LEAN_CLOSURE: u8 = 245;
30pub const LEAN_ARRAY: u8 = 246;
31pub const LEAN_STRUCT_ARRAY: u8 = 247;
32pub const LEAN_SCALAR_ARRAY: u8 = 248;
33pub const LEAN_STRING: u8 = 249;
34pub const LEAN_MPZ: u8 = 250;
35pub const LEAN_THUNK: u8 = 251;
36pub const LEAN_TASK: u8 = 252;
37pub const LEAN_REF: u8 = 253;
38pub const LEAN_EXTERNAL: u8 = 254;
39pub const LEAN_RESERVED: u8 = 255;
40
41// Object-allocator constants — `lean.h:30–32`.
42pub const LEAN_CLOSURE_MAX_ARGS: usize = 16;
43pub const LEAN_OBJECT_SIZE_DELTA: usize = 8;
44pub const LEAN_MAX_SMALL_OBJECT_SIZE: usize = 4096;
45
46// Constructor-shape ceilings — `lean.h:97–98`.
47pub const LEAN_MAX_CTOR_FIELDS: usize = 256;
48pub const LEAN_MAX_CTOR_SCALARS_SIZE: usize = 1024;
lean_rs_sys/consts.rs

lean_rs_sys/
consts.rs
