lean-rs-sys 0.3.1

Raw FFI bindings for the Lean 4 C ABI. See `lean-rs` for the safe front door.
Documentation 
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17

//! Runtime memory guardrail entry points.
//!
//! These symbols are exported by `libleanshared` but are not part of
//! `lean.h`'s object ABI. They configure Lean's best-effort memory checks;
//! they do not reclaim retained runtime state.

unsafe extern "C" {
    /// Set Lean's process-global maximum memory in bytes.
    ///
    /// # Safety
    ///
    /// This changes process-global Lean runtime state. Callers must ensure
    /// they are configuring an isolated worker/profiling process or otherwise
    /// understand that every later Lean runtime check in the process observes
    /// the new limit.
    pub fn lean_internal_set_max_memory(max: usize) -> crate::lean_obj_res;
}