lean_rs/runtime/mod.rs
1//! Process-wide Lean runtime anchor.
2//!
3//! The L1 lifetime-bound owned-object handle [`obj::Obj`] (with its
4//! borrowed view [`obj::ObjRef`]) is `pub` here so the sibling
5//! `lean-rs-host` crate can wrap them inside its host-defined handle
6//! types. The init cell and thread-attach helpers stay `pub(crate)` —
7//! callers reach them through [`LeanRuntime::init`] and
8//! [`LeanThreadGuard::attach`] re-exported at the crate root.
9//!
10//! What this layer hides from the rest of the crate:
11//!
12//! - which raw `lean_rs_sys` symbols implement init and thread attach;
13//! - the order in which those symbols must be called;
14//! - the `OnceLock` cell that makes initialization process-once;
15//! - the `catch_unwind` boundary that keeps Rust panics from unwinding
16//! into Lean or C frames;
17//! - the `lean_inc` / `lean_dec` discipline behind every owned or
18//! borrowed Lean object handle.
19
20pub(crate) mod init;
21pub mod obj;
22pub(crate) mod thread;
23
24pub use init::LeanRuntime;
25pub use thread::LeanThreadGuard;
26
27#[cfg(test)]
28mod tests;