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.