lean_rs_sys/
memory.rs

1//! Runtime memory guardrail entry points.
2//!
3//! These symbols are exported by `libleanshared` but are not part of
4//! `lean.h`'s object ABI. They configure Lean's best-effort memory checks;
5//! they do not reclaim retained runtime state.
6
7unsafe extern "C" {
8    /// Set Lean's process-global maximum memory in bytes.
9    ///
10    /// # Safety
11    ///
12    /// This changes process-global Lean runtime state. Callers must ensure
13    /// they are configuring an isolated worker/profiling process or otherwise
14    /// understand that every later Lean runtime check in the process observes
15    /// the new limit.
16    pub fn lean_internal_set_max_memory(max: usize) -> crate::lean_obj_res;
17}
lean_rs_sys/memory.rs

lean_rs_sys/
memory.rs
