Struct LeanSession 

pub struct LeanSession<'lean, 'c> { /* private fields */ }

A long-lived Lean session over an imported environment.

Construct via LeanCapabilities::session. The session owns the imported Lean.Environment privately (never exposed) and dispatches each typed query through the capability’s pre-resolved symbol addresses. Neither Send nor Sync: inherited from the contained Obj<'lean> and the borrow of LeanCapabilities.

Implementations

impl<'lean, 'c> LeanSession<'lean, 'c>

pub fn stats(&self) -> SessionStats

Snapshot of this session’s accumulated dispatch metrics.

Returns a copy; the counters keep accumulating after the call. Use SessionStats::default to compute a delta across two snapshots.

pub fn query_declaration( &mut self, name: &str, cancellation: Option<&LeanCancellationToken>, ) -> LeanResult<LeanDeclaration<'lean>>

Look up a declaration by full Lean name (e.g. "Nat.zero").

Errors

Returns lean_rs::LeanError::Host with stage HostStage::Conversion if the name is not present in the imported environment. Returns lean_rs::LeanError::LeanException if the Lean-side query raises.

pub fn list_declarations( &mut self, cancellation: Option<&LeanCancellationToken>, ) -> LeanResult<Vec<LeanName<'lean>>>

All declaration names in the imported environment.

Returns a Vec; the environment’s constants map contains many thousands of entries even for a small project (Lean prelude is always imported), so prefer LeanSession::query_declaration when you already know the name.

Errors

Returns lean_rs::LeanError::LeanException if the Lean-side query raises.

pub fn list_declarations_filtered( &mut self, filter: &LeanDeclarationFilter, cancellation: Option<&LeanCancellationToken>, progress: Option<&dyn LeanProgressSink>, ) -> LeanResult<Vec<LeanName<'lean>>>

Declaration names matching filter.

Filtering runs inside Lean while traversing the environment constants table, so Rust only allocates handles for names the caller asked to keep.

Errors

Returns lean_rs::LeanError::Cancelled if cancellation is already cancelled before dispatch. Returns lean_rs::LeanError::LeanException if the Lean-side query raises.

pub fn declaration_source_range( &mut self, name: &str, cancellation: Option<&LeanCancellationToken>, ) -> LeanResult<Option<LeanSourceRange>>

Source range Lean recorded for name.

Returns Ok(None) when the name is absent or Lean has no declaration range for it. That is normal for synthetic, runtime-created, and some compiler-generated declarations.

Errors

Returns lean_rs::LeanError::Cancelled if cancellation is already cancelled before dispatch. Returns lean_rs::LeanError::LeanException if the Lean-side query raises.

pub fn declaration_type( &mut self, name: &str, cancellation: Option<&LeanCancellationToken>, ) -> LeanResult<Option<LeanExpr<'lean>>>

The declared type of name, as an opaque LeanExpr handle.

Returns Ok(None) if the name is not present in the environment.

Errors

Returns lean_rs::LeanError::LeanException if the Lean-side query raises.

pub fn declaration_type_bulk( &mut self, names: &[&str], cancellation: Option<&LeanCancellationToken>, progress: Option<&dyn LeanProgressSink>, ) -> LeanResult<Vec<Option<LeanExpr<'lean>>>>

The declared types of names, preserving input order.

Returns None in each slot whose name is not present in the environment. With cancellation = None, the whole batch crosses the FFI boundary once and Lean converts the input strings to names internally. With Some(token), this loops through Self::declaration_type so cancellation can be observed between items; partial results are discarded when cancellation fires.

Errors

Returns lean_rs::LeanError::LeanException if the Lean-side bulk shim raises through IO.

pub fn declaration_kind( &mut self, name: &str, cancellation: Option<&LeanCancellationToken>, ) -> LeanResult<String>

The kind of name as a Lean-rendered string ("axiom", "definition", "theorem", "opaque", "quot", "inductive", "constructor", "recursor"), or "missing" if name is not in the environment.

Errors

Returns lean_rs::LeanError::LeanException if the Lean-side query raises.

pub fn declaration_kind_bulk( &mut self, names: &[&str], cancellation: Option<&LeanCancellationToken>, progress: Option<&dyn LeanProgressSink>, ) -> LeanResult<Vec<String>>

The declaration kinds of names, preserving input order.

Each output slot is the same string that Self::declaration_kind would return for the corresponding input, including "missing" for absent declarations. With cancellation = None, this is one Lean-side bulk dispatch over an Array String; with Some(token), this loops through the singular path so the token can be checked between items.

Errors

Returns lean_rs::LeanError::LeanException if the Lean-side bulk shim raises through IO.

pub fn declaration_name( &mut self, name: &str, cancellation: Option<&LeanCancellationToken>, ) -> LeanResult<String>

The Lean-rendered display string of name. Round-trips a name through the capability’s Name.toString shim so callers see the same canonical form Lean would log.

Diagnostic only — not a semantic key. Use LeanSession::query_declaration + a typed handle when equality matters.

Errors

Returns lean_rs::LeanError::LeanException if the Lean-side query raises.

pub fn declaration_name_bulk( &mut self, names: &[&str], cancellation: Option<&LeanCancellationToken>, progress: Option<&dyn LeanProgressSink>, ) -> LeanResult<Vec<String>>

Lean-rendered display strings for names, preserving input order.

This is diagnostic text, not a semantic key. Missing declarations are not an error because the singular Self::declaration_name path also only round-trips the input name through Lean’s Name.toString renderer.

With cancellation = None, this is one Lean-side bulk dispatch over an Array String; with Some(token), this loops through the singular path so the token can be checked between items.

Errors

Returns lean_rs::LeanError::LeanException if the Lean-side bulk shim raises through IO.

pub fn elaborate( &mut self, source: &str, expected_type: Option<&LeanExpr<'lean>>, options: &LeanElabOptions, cancellation: Option<&LeanCancellationToken>, ) -> LeanResult<Result<LeanExpr<'lean>, LeanElabFailure>>

Parse and elaborate a single Lean term against the imported environment, optionally against an expected type.

The boundary is explicit: Rust supplies the source text, module context, and bounded options; Lean parses, elaborates, and returns either an opaque LeanExpr handle or a structured LeanElabFailure carrying typed diagnostics. Rust does not inspect elaborator internals or proof terms to decide correctness.

The outer LeanResult surfaces host-stack failures (a Lean IO-level exception from the shim itself, a malformed Lean return value); the inner Result distinguishes successful elaboration from parse / type / kernel-stage failures the elaborator reports through its MessageLog. Both error paths propagate the LeanElabOptions::diagnostic_byte_limit bound structurally.

Errors

Returns lean_rs::LeanError::LeanException if the Lean-side shim raises through IO. Returns lean_rs::LeanError::Host with stage HostStage::Conversion if the Lean return value does not decode into LeanElabFailure / LeanExpr.

pub fn kernel_check( &mut self, source: &str, options: &LeanElabOptions, cancellation: Option<&LeanCancellationToken>, progress: Option<&dyn LeanProgressSink>, ) -> LeanResult<LeanKernelOutcome<'lean>>

Parse, elaborate, and kernel-check a Lean declaration source (typically a theorem or def), returning a typed outcome that classifies the result and carries either the produced crate::LeanEvidence handle or the diagnostics the elaborator and kernel emitted.

The boundary is explicit (mirrors Self::elaborate): Rust supplies source + options; Lean parses, elaborates, runs addDecl (which kernel-checks), and classifies the outcome. Rust never inspects the produced proof term or declaration internals.

Errors

Returns lean_rs::LeanError::LeanException if the Lean-side shim raises through IO (an unexpected internal failure that is not itself a rejection / unavailable diagnostic). Returns lean_rs::LeanError::Host with stage HostStage::Conversion if the Lean return value does not decode into LeanKernelOutcome.

pub fn check_evidence( &mut self, handle: &LeanEvidence<'lean>, cancellation: Option<&LeanCancellationToken>, ) -> LeanResult<EvidenceStatus>

Re-validate a previously captured LeanEvidence against the session’s imported environment, returning the kernel’s current verdict.

The handle was produced by an earlier Self::kernel_check call against this same environment and carries the kernel-accepted Lean.Declaration opaquely. The session never installs that declaration into its stored environment, so re-checking against the unchanged environment is the supported way to ask “is this evidence still valid?” — the kernel runs fresh.

The returned EvidenceStatus mirrors LeanKernelOutcome::status: Checked on success, Rejected if the kernel now refuses the declaration, Unavailable if the Lean shim caught an IO exception. The Lean fixture does not currently emit Unsupported from this path — Unsupported only fires during the initial classification in kernel_check.

Errors

Returns lean_rs::LeanError::LeanException if the Lean shim raises through IO outside of its own try (an unexpected internal failure that the shim did not classify). Returns lean_rs::LeanError::Host with stage HostStage::Conversion if the return value does not decode as a four-tag EvidenceStatus inductive.

pub fn summarize_evidence( &mut self, handle: &LeanEvidence<'lean>, cancellation: Option<&LeanCancellationToken>, ) -> LeanResult<ProofSummary>

Project a previously captured LeanEvidence into a bounded ProofSummary for diagnostics or storage.

The Lean shim renders the captured declaration’s name, kind, and type expression as three byte-bounded Strings — no Lean.Expr or proof term crosses the FFI boundary. The summary is computed on demand (not at Self::kernel_check time) because most callers only ever inspect the EvidenceStatus tag and would pay the pretty-print cost for nothing.

Strings on the returned summary are display text. They are not semantic keys; route equality comparisons through a Lean-authored equality export.

Errors

Returns lean_rs::LeanError::LeanException if the Lean shim raises through IO. Returns lean_rs::LeanError::Host with stage HostStage::Conversion if the return value does not decode as a three-field ProofSummary structure.

pub fn run_meta<Req, Resp>( &mut self, service: &LeanMetaService<Req, Resp>, request: Req, options: &LeanMetaOptions, cancellation: Option<&LeanCancellationToken>, ) -> LeanResult<LeanMetaResponse<Resp>>

where Req: LeanAbi<'lean>, Resp: TryFromLean<'lean>,

Invoke a registered bounded MetaM service against the imported environment.

The session looks up the service’s cached address; if the loaded capability does not export the symbol, the call short- circuits to LeanMetaResponse::Unsupported with a synthetic host-side diagnostic naming the missing symbol. Otherwise the session constructs a per-call typed LeanExported handle over the meta service’s (Environment, Req, UInt64, USize, UInt8) -> IO (MetaResponse Resp) signature and dispatches.

The outer LeanResult surfaces host-stack failures (a Lean IO-level exception from the shim itself, or an undecodable return value). The four-way classification — Ok / Failed / TimeoutOrHeartbeat / Unsupported — lives in the inner LeanMetaResponse.

Errors

Returns lean_rs::LeanError::LeanException if the Lean shim raises through IO. Returns lean_rs::LeanError::Host with stage HostStage::Conversion if the return value does not decode into LeanMetaResponse<Resp>.

pub fn query_declarations_bulk( &mut self, names: &[&str], cancellation: Option<&LeanCancellationToken>, progress: Option<&dyn LeanProgressSink>, ) -> LeanResult<Vec<LeanDeclaration<'lean>>>

Look up many declarations in one Lean traversal.

Equivalent to calling Self::query_declaration in a loop over names, except that the entire batch crosses the FFI boundary exactly once: one Array Name allocation in, one Array (Option Declaration) allocation out. The Lean shim folds the singular envQueryDeclaration across the input array, so the iteration semantics are identical to a Rust-side fold over the singular path — a missing name still errors the batch.

Names are still resolved through the capability’s name_from_string shim, one lean_rs::LeanName handle per input. The metric impact is names.len() + 1 recorded FFI calls for a batch of names.len() items, versus 2 * names.len() for the same workload through Self::query_declaration.

Errors

Returns lean_rs::LeanError::Host with stage HostStage::Conversion on the first name that is not present in the imported environment, with the missing name in the diagnostic. Returns lean_rs::LeanError::LeanException if the Lean-side bulk shim raises through IO.

pub fn elaborate_bulk( &mut self, sources: &[&str], options: &LeanElabOptions, cancellation: Option<&LeanCancellationToken>, progress: Option<&dyn LeanProgressSink>, ) -> LeanResult<Vec<Result<LeanExpr<'lean>, LeanElabFailure>>>

Parse and elaborate many independent Lean terms in one Lean traversal.

Per-source Result<LeanExpr, LeanElabFailure> shape matches Self::elaborate exactly: outer LeanResult surfaces host-stack failures, inner per-source Result distinguishes successful elaboration from elaborator-reported diagnostics. A caller treating the bulk path as a fold over the singular path sees no semantic surprise.

The expected_type parameter is not carried by the bulk shape: per-source expectations would force a parallel &[Option<&LeanExpr>] array, and no in-tree caller has earned the surface. Use Self::elaborate for individual terms with expected types.

The heartbeat and diagnostic-byte budgets in options apply once each per source (the Lean shim builds fresh Lean.Options per item via the same hostElaborate path), so the per-batch upper bound on elapsed CPU work is sources.len() * options.heartbeats().

Errors

Returns lean_rs::LeanError::LeanException if the Lean-side bulk shim raises through IO. Returns lean_rs::LeanError::Host with stage HostStage::Conversion if the Lean return value does not decode into a Vec<Result<LeanExpr, LeanElabFailure>>.

pub fn call_capability<Args, R>( &mut self, name: &str, args: Args, cancellation: Option<&LeanCancellationToken>, ) -> LeanResult<R::Output>

where Args: LeanArgs<'lean>, R: DecodeCallResult<'lean>,

Look up and invoke a capability-exported function by name with a typed argument tuple and a typed result decoder.

This is the transport-neutral escape hatch for capability dylibs that export Lean functions beyond the twenty-six session-fixed symbols. The conversion bounds — LeanArgs on the argument tuple and DecodeCallResult on the result — are the same bounds lean_rs::module::LeanModule::exported uses, so an IO-returning Lean capability is invoked with R = LeanIo<T> (fused decode_io + T::try_from_lean) and a pure capability with R = T for T: LeanAbi. The sealed traits stay invisible at the call site; the bound is satisfied automatically.

Function-only: nullary-constant globals are not capabilities. Reach a Lean nullary-constant global directly through lean_rs::module::LeanModule::exported if you need one. The symbol address is resolved on every call (one dlsym per invocation); for hot capabilities, prefer pre-resolving via LeanModule::exported and caching the lean_rs::module::LeanExported handle.

Errors

Returns lean_rs::LeanError::Host with stage HostStage::Link if name does not resolve as a function symbol in the capability dylib. Returns lean_rs::LeanError::LeanException when the underlying Lean export raises through IO (only possible when R = LeanIo<_>). Returns lean_rs::LeanError::Host with stage HostStage::Conversion when the return value does not decode into the declared R::Output.