lean-rs 0.6.0

Safe Rust bindings for Lean 4 interop: runtime initialization, object handles, typed ABI conversions, module loading, exported function calls, semantic handles, and callback handles.
Documentation 
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25

//! Process-global Lean runtime memory guardrails.
//!
//! This is intentionally separate from runtime initialization and object
//! ownership. The setter does not reclaim memory; it only configures Lean's
//! periodic runtime memory check.
//!
//! The check is not recoverable from Rust. Lean signals an overrun by throwing a
//! C++ exception, and it cannot unwind through the Rust frame that called into
//! Lean: the process aborts with `fatal runtime error: Rust cannot catch foreign
//! exceptions`. Treat the limit as a contained-abort guardrail — better than an
//! OS OOM-kill of the whole machine — not as a way to turn a runaway elaboration
//! into an error value.

// SAFETY DOC: this module is the narrow safe wrapper around Lean's raw
// process-global memory-limit setter.
#![allow(unsafe_code)]

pub(crate) fn set_memory_limit_bytes_for_guardrail(limit_bytes: usize) {
    // SAFETY: callers route through the hidden sibling-crate bridge and use
    // this only for isolated worker/profiling processes. The call mutates
    // process-global Lean runtime state.
    unsafe {
        let _ = lean_rs_sys::memory::lean_internal_set_max_memory(limit_bytes);
    }
}