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 checked host-shim bindings resolved during construction. 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 import_stats(&self) -> &LeanImportStats

Lean-native attribution for this session’s imported environment.

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 search_declarations( &mut self, search: &DeclarationSearchRequest, cancellation: Option<&LeanCancellationToken>, ) -> LeanResult<DeclarationSearchResult>

Search declarations with structural filters and bounded metadata rows.

The search runs inside Lean while traversing the imported environment. It may inspect declaration types structurally for required constants and conclusion heads, but it never renders type text. Use Self::declaration_type for explicit one-name type rendering.

Errors

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

pub fn inspect_declaration( &mut self, request: &DeclarationInspectionRequest, cancellation: Option<&LeanCancellationToken>, ) -> LeanResult<DeclarationInspectionResult>

Inspect one selected declaration under explicit output budgets.

Search remains metadata-only; callers use this method after selecting one declaration name whose rendered statement/docstring are worth paying for. Missing names and missing optional shim support are normal result statuses.

Errors

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

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_module_query( &mut self, source: &str, query: &ModuleQuery, options: &LeanElabOptions, cancellation: Option<&LeanCancellationToken>, ) -> LeanResult<ModuleQueryOutcome>

Parse and elaborate a Lean module, returning only the requested bounded projection.

The Lean shim owns header parsing, module-system header handling, info-tree traversal, cursor selection, reference collection, and bounded expression/goal rendering. The Rust side chooses a ModuleQuery and receives the matching ModuleQueryOutcome; whole-file raw expression/type dumps never cross this boundary.

The shim is optional. When the loaded capability dylib does not export lean_rs_host_process_module_query, the method returns ModuleQueryOutcome::Unsupported without an FFI call.

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

pub fn process_module_query_batch( &mut self, source: &str, selectors: &[ModuleQuerySelector], budgets: &ModuleQueryOutputBudgets, options: &LeanElabOptions, cancellation: Option<&LeanCancellationToken>, ) -> LeanResult<ModuleQueryBatchOutcome>

Parse and elaborate a Lean module once, returning several bounded projections keyed by selector id.

This is the proof-agent path: Lean owns header handling, one body elaboration, info-tree traversal, and selector projection. Rust sends a small selector array and receives per-selector outcomes; whole-file info-tree arrays never cross the boundary.

The shim is optional. When the loaded capability dylib does not export lean_rs_host_process_module_query_batch, the method returns ModuleQueryBatchOutcome::Unsupported without an FFI call.

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

pub fn process_module_query_batch_cached( &mut self, source: &str, selectors: &[ModuleQuerySelector], budgets: &ModuleQueryOutputBudgets, options: &LeanElabOptions, policy: &ModuleQueryCachePolicy, cancellation: Option<&LeanCancellationToken>, ) -> LeanResult<ModuleQueryBatchCachedOutcome>

Parse/elaborate a Lean module through the shim-owned module snapshot cache, then return bounded selector projections plus cache facts.

The snapshot cache remains private to the loaded shim. Rust provides the stable cache key and conservative policy, but never receives raw info trees.

Errors

Returns an error if cancellation is already requested, if the shim raises an IO exception, or if the Lean result cannot be decoded into the expected cached batch outcome.

pub fn attempt_proof( &mut self, request: &ProofAttemptRequest, options: &LeanElabOptions, cancellation: Option<&LeanCancellationToken>, ) -> LeanResult<ProofAttemptOutcome>

Try proof snippets against an in-memory source overlay.

The shim is optional. When the loaded capability dylib does not export lean_rs_host_attempt_proof, the method returns ProofAttemptOutcome::Unsupported without an FFI call.

Errors

Returns an error if cancellation is already requested, if the shim raises an IO exception, or if the Lean result cannot be decoded.

pub fn verify_declaration( &mut self, request: &DeclarationVerificationRequest, options: &LeanElabOptions, cancellation: Option<&LeanCancellationToken>, ) -> LeanResult<DeclarationVerificationOutcome>

Verify one declaration in an in-memory source snapshot.

The shim is optional. When the loaded capability dylib does not export lean_rs_host_verify_declaration, the method returns DeclarationVerificationOutcome::Unsupported without an FFI call.

Errors

Returns an error if cancellation is already requested, if the shim raises an IO exception, or if the Lean result cannot be decoded.

pub fn verify_declaration_batch( &mut self, request: &DeclarationVerificationBatchRequest, options: &LeanElabOptions, cancellation: Option<&LeanCancellationToken>, ) -> LeanResult<DeclarationVerificationBatchOutcome>

Verify several declarations in one in-memory source snapshot.

The shim is optional. When the loaded capability dylib does not export lean_rs_host_verify_declaration_batch, the method returns DeclarationVerificationBatchOutcome::Unsupported without an FFI call. The returned rows preserve request order.

Errors

Returns an error if cancellation is already requested, if the shim raises an IO exception, or if the Lean result cannot be decoded.

pub fn clear_module_snapshot_cache( &mut self, ) -> LeanResult<ModuleSnapshotCacheClearResult>

Clear the shim-owned module snapshot cache when the loaded capability supports it.

This releases only cached module snapshots built by the bundled info-tree shim. It does not reset Lean’s runtime, unload imported modules, or make full-session compacted regions safe to free.

Errors

Returns an error if the shim raises an IO exception or if the Lean clear result cannot be decoded.

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 LeanMetaService<Req, Resp>: HostMetaDispatch<'lean, Req, Resp>, Req: LeanAbi<'lean>, Resp: TryFromLean<'lean>,

Invoke a registered bounded MetaM service against the imported environment.

The session dispatches through the checked binding for the closed service shape; if the loaded capability does not export the optional symbol, the call short-circuits to LeanMetaResponse::Unsupported with a synthetic host-side diagnostic naming the missing symbol.

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