Struct LeanRuntime 

pub struct LeanRuntime { /* private fields */ }

Handle for the process-wide Lean runtime.

LeanRuntime is a zero-sized type with no public constructor. The only way to obtain one is to call LeanRuntime::init, which returns a 'static borrow once the Lean runtime is up. Every later handle (Obj<'lean>, LeanExpr<'lean>, LeanSession<'lean, '_>, …) carries a 'lean lifetime tied to this borrow, so a value derived from Lean cannot outlive the runtime that produced it. This is the type-system anchor for the 'lean cascade described in docs/architecture/03-host-stack.md.

Neither Send nor Sync. The Lean runtime is per-thread, and shipping a Lean-derived handle to another OS thread is a soundness hazard rather than an ergonomic choice; the !Sync claim here forces &'lean LeanRuntime to be !Send, and every downstream handle that holds PhantomData<&'lean LeanRuntime> inherits the same restriction.

Implementations

impl LeanRuntime

pub fn init() -> LeanResult<&'static Self>

Initialize the Lean runtime if it has not already been initialized, and return a 'static borrow that anchors the 'lean lifetime cascade.

Idempotent and safe to call from any thread: the underlying initialization runs exactly once for the lifetime of the process. Subsequent calls—including calls from other threads—return the same borrow, or replay the cached failure if the first attempt failed.

Worker threads

init starts a process-wide Lean task manager. The worker thread count is Lean’s compiled-in default—typically one worker per hardware core—unless the LEAN_RS_NUM_THREADS environment variable is set to a positive integer before the first call to init. The first call captures the value; later changes to the variable have no effect. Set LEAN_RS_NUM_THREADS when several Lean-using processes run side by side (CI test matrices, batch jobs, multi-tenant workers) to avoid oversubscribing cores. The pool is process-lifetime; there is no set_num_threads-style reconfiguration once init has run.

Errors

Returns a LeanError::Host with stage HostStage::RuntimeInit if initialization failed. Today the only reachable failure is a caught panic from the Lean lean_initialize_* entry points; the panic payload is rendered into a bounded message so it cannot unwind into Lean or C frames.

Trait Implementations

impl Debug for LeanRuntime

fn fmt(&self, f: &mut Formatter<'_>) -> Result

Formats the value using the given formatter.