Struct PooledSession 

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

A LeanSession borrowed from a SessionPool.

Behaves as a LeanSession through core::ops::Deref / core::ops::DerefMut — every session method is reachable directly:

let pool = lean_rs::SessionPool::with_capacity(runtime, 4);
let mut sess = pool.acquire(&caps, &["MyLib"], None, None)?;
let kind = sess.declaration_kind("MyLib.thing", None)?;
// dropping `sess` returns the imported environment to the pool

On Drop, the underlying imported environment is returned to the pool (or released if the pool is at capacity). Per-session crate::host::session::SessionStats are scoped to the lifetime of this checkout — they start at zero on every acquire and are inaccessible after release.

Three lifetimes: 'lean (runtime), 'p (pool borrow), 'c (capability borrow). Neither Send nor Sync (inherited from the contained LeanSession).

Methods from Deref<Target = 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 name_to_string( &mut self, name: &LeanName<'lean>, cancellation: Option<&LeanCancellationToken>, ) -> LeanResult<String>

Render an opaque LeanName handle as its dotted-string form, routed through the capability’s Name.toString shim.

This is the supported way to turn a LeanName (e.g. an element of Self::list_declarations_filtered’s result) into Rust text. The output is diagnostic — not a semantic key — and equality on the underlying Lean.Name still lives in Lean.

Errors

Returns lean_rs::LeanError::Cancelled if cancellation is already cancelled before dispatch.

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

Render names as dotted-string forms, preserving input order.

Implemented as a per-item loop over Self::name_to_string in v1: cancellation is checked between items, progress is reported after each. The Lean shim is pure and short, so the per-item FFI overhead is acceptable; a bulk shim is a future optimisation if profiling shows it matters.

Errors

Returns lean_rs::LeanError::Cancelled between items if the token is tripped during the walk.

pub fn list_declarations_strings( &mut self, filter: &LeanDeclarationFilter, cancellation: Option<&LeanCancellationToken>, progress: Option<&dyn LeanProgressSink>, ) -> LeanResult<Vec<String>>

Enumerate the imported environment’s declaration names and render each as a dotted string. Convenience over Self::list_declarations_filtered + Self::name_to_string_bulk for the common case where the consumer only needs strings.

Two FFI hops (list + per-name render) and one heap allocation per name. For batches under a few thousand this is fine; for six-figure walks consider the lower-level pair so the listing pass and the rendering pass can be cancelled or chunked independently.

Errors

Forwards errors from Self::list_declarations_filtered and Self::name_to_string_bulk.

pub fn expr_to_string_raw( &mut self, expr: &LeanExpr<'lean>, cancellation: Option<&LeanCancellationToken>, ) -> LeanResult<String>

Render expr via Expr.toString — the cheap, deterministic projection.

Walks the syntax tree directly: no MetaM, no notation lookup, no binder pretty-printing. The result is a legible-but-ugly dump suitable for indexing, logging, and search keys. For the form a Lean user reads, use the optional crate::host::meta::pp_expr service through Self::run_meta instead — it pays for elaboration context to get notation and unfolding right but can time out under a tight heartbeat budget.

Errors

Returns lean_rs::LeanError::Cancelled if cancellation is already cancelled before dispatch.

pub fn process_with_info_tree( &mut self, source: &str, options: &LeanElabOptions, cancellation: Option<&LeanCancellationToken>, ) -> LeanResult<ProcessFileOutcome>

Parse, elaborate, and project a Lean source string into its Elab.InfoTree.

Drives Lean’s IO.processCommands pipeline with info collection enabled, walks every captured info tree, and projects each TermInfo / TacticInfo / CommandInfo / identifier reference into a ProcessedFile value. The projection is the FFI boundary — raw InfoTree does not cross, because it carries metavariable contexts that cannot be revived outside the session that produced them.

Goal text in TacticInfoNode::goals_before / TacticInfoNode::goals_after is pre-rendered through Lean’s Meta.ppGoal inside the elaboration context; the cumulative goal-byte sum is bounded by LeanElabOptions::diagnostic_byte_limit.

The shim is optional. When the loaded capability dylib does not export lean_rs_host_process_with_info_tree, the method returns ProcessFileOutcome::Unsupported without an FFI call — matching the meta-service degradation pattern. There is no separate timeout arm because IO.processCommands catches per-command exceptions and attaches them to the message log; inspect ProcessedFile::diagnostics to detect heartbeat exhaustion.

Errors

Returns lean_rs::LeanError::Cancelled if cancellation is already cancelled before dispatch. 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 ProcessedFile.

pub fn process_module_with_info_tree( &mut self, source: &str, options: &LeanElabOptions, cancellation: Option<&LeanCancellationToken>, ) -> LeanResult<ProcessModuleOutcome>

Parse a Lean source file’s header, then resume elaboration of the body against the session’s open env, returning the info-tree projection in the original file’s coordinate system.

Unlike Self::process_with_info_tree (which is right for header-less snippets), this method calls Lean.Parser.parseHeader first and resumes IO.processCommands from the parser state the header parser produced. The shared InputContext.fileMap covers the whole source, so positions in the returned ProcessedFile use the original file’s line and column numbers with no Rust-side offset arithmetic.

Three real outcomes plus an Unsupported degradation arm:

• ProcessModuleOutcome::Ok — header parsed; every user-written import is present in the session’s open env; the body was processed. imports lists the user-written modules (Lean’s auto-inserted Init is filtered out by the shim).
• ProcessModuleOutcome::MissingImports — header parsed but some imports name modules the open env lacks. The body still elaborated against whatever the env carries; the projection is populated and missing lists the absent modules. Soft failure — callers typically surface it as a warning rather than as an error.
• ProcessModuleOutcome::HeaderParseFailed — the header itself did not parse (e.g. a malformed import line). IO.processCommands was not run; only the header diagnostics are returned.
• ProcessModuleOutcome::Unsupported — the loaded capability dylib does not export lean_rs_host_process_module_with_info_tree. No FFI call was made.

As with Self::process_with_info_tree, heartbeat exhaustion during a single command’s elaboration surfaces as an error-severity entry in ProcessedFile::diagnostics rather than as a separate wire arm.

Errors

Returns lean_rs::LeanError::Cancelled if cancellation is already cancelled before dispatch. 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 ProcessModuleOutcome.

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-eight 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.

Trait Implementations

impl Debug for PooledSession<'_, '_, '_>

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

Formats the value using the given formatter.

impl<'lean, 'c> Deref for PooledSession<'lean, '_, 'c>

type Target = LeanSession<'lean, 'c>

The resulting type after dereferencing.

fn deref(&self) -> &Self::Target

Dereferences the value.

impl<'lean, 'c> DerefMut for PooledSession<'lean, '_, 'c>

fn deref_mut(&mut self) -> &mut LeanSession<'lean, 'c>

Mutably dereferences the value.

impl Drop for PooledSession<'_, '_, '_>

fn drop(&mut self)

Executes the destructor for this type.

fn pin_drop(self: Pin<&mut Self>)

🔬This is a nightly-only experimental API. (pin_ergonomics)

Execute the destructor for this type, but different to Drop::drop, it requires self to be pinned.