Struct LeanWorkerSession 

pub struct LeanWorkerSession<'worker> { /* private fields */ }

Narrow host-session adapter over a live LeanWorker.

Dropping this value does not stop the worker. If a request is cancelled while in flight, the supervisor cycles the child process and this session is invalidated; open a fresh session before issuing more host requests.

Implementations

impl LeanWorkerSession<'_>

pub fn request_timeout(&self) -> Duration

Return the timeout used for subsequent requests on this session.

pub fn set_request_timeout(&mut self, timeout: Duration)

Change the timeout for subsequent requests on this session.

A timeout is parent-enforced. If it fires, the supervisor kills and replaces the child process and invalidates this session.

pub fn elaborate( &mut self, source: &str, options: &LeanWorkerElabOptions, cancellation: Option<&LeanWorkerCancellationToken>, progress: Option<&dyn LeanWorkerProgressSink>, ) -> Result<LeanWorkerElabResult, LeanWorkerError>

Elaborate one term and return only process-safe success/diagnostic data.

Errors

Returns LeanWorkerError if the worker is dead, the child reports a host error, cancellation is observed, a progress sink panics, or protocol communication fails.

pub fn kernel_check( &mut self, source: &str, options: &LeanWorkerElabOptions, cancellation: Option<&LeanWorkerCancellationToken>, progress: Option<&dyn LeanWorkerProgressSink>, ) -> Result<LeanWorkerKernelResult, LeanWorkerError>

Kernel-check one declaration and return only process-safe status/diagnostics.

Errors

Returns LeanWorkerError if the worker is dead, the child reports a host error, cancellation is observed, a progress sink panics, or protocol communication fails.

pub fn declaration_kinds( &mut self, names: &[&str], cancellation: Option<&LeanWorkerCancellationToken>, progress: Option<&dyn LeanWorkerProgressSink>, ) -> Result<Vec<String>, LeanWorkerError>

Query declaration kinds in bulk.

Errors

Returns LeanWorkerError if the worker is dead, the child reports a host error, cancellation is observed, a progress sink panics, or protocol communication fails.

pub fn declaration_names( &mut self, names: &[&str], cancellation: Option<&LeanWorkerCancellationToken>, progress: Option<&dyn LeanWorkerProgressSink>, ) -> Result<Vec<String>, LeanWorkerError>

Render declaration names in bulk.

Errors

Returns LeanWorkerError if the worker is dead, the child reports a host error, cancellation is observed, a progress sink panics, or protocol communication fails.

pub fn infer_type( &mut self, source: &str, options: &LeanWorkerElabOptions, cancellation: Option<&LeanWorkerCancellationToken>, progress: Option<&dyn LeanWorkerProgressSink>, ) -> Result<LeanWorkerMetaResult<LeanWorkerRendered>, LeanWorkerError>

Elaborate source and infer the resulting expression’s type.

The child attempts notation-aware rendering via the optional meta_pp_expr shim (Lean.PrettyPrinter.ppExpr) and falls back to Expr.toString when the shim is absent or reports Unsupported. The returned LeanWorkerRendered::rendering reports which path produced the value.

Heartbeat budgeting: each MetaM pass (the primary inferType call and the pretty-printer) runs under the same LeanWorkerElabOptions::heartbeat_limit value, independently bounded—the pretty-printer does not consume budget left over from the primary call. A Failed or TimeoutOrHeartbeat reported by the pretty-printer surfaces as the whole call’s failure (matching in-process behaviour); there is no path that returns the inferred expression alongside a pretty-printer failure. Only Unsupported from pp_expr triggers the raw fallback.

Errors

Returns LeanWorkerError if the worker is dead, the child reports a host error, cancellation is observed, a progress sink panics, or protocol communication fails. Lean-side failures (type errors, heartbeat exhaustion, missing capability) surface inside the returned LeanWorkerMetaResult rather than as Err.

pub fn whnf( &mut self, source: &str, options: &LeanWorkerElabOptions, cancellation: Option<&LeanWorkerCancellationToken>, progress: Option<&dyn LeanWorkerProgressSink>, ) -> Result<LeanWorkerMetaResult<LeanWorkerRendered>, LeanWorkerError>

Elaborate source and reduce it to weak head normal form.

Rendering and heartbeat-budgeting semantics match Self::infer_type: the child attempts notation-aware rendering via meta_pp_expr and falls back to Expr.toString when the shim reports Unsupported. Each MetaM pass is independently bounded by heartbeat_limit; a Failed or TimeoutOrHeartbeat from the pretty-printer surfaces as the whole call’s failure.

Errors

Returns LeanWorkerError under the same conditions as Self::infer_type. Lean-side failures surface inside the returned LeanWorkerMetaResult.

pub fn is_def_eq( &mut self, lhs: &str, rhs: &str, transparency: LeanWorkerMetaTransparency, options: &LeanWorkerElabOptions, cancellation: Option<&LeanWorkerCancellationToken>, progress: Option<&dyn LeanWorkerProgressSink>, ) -> Result<LeanWorkerMetaResult<bool>, LeanWorkerError>

Elaborate lhs and rhs and ask Lean whether they are definitionally equal at the supplied transparency.

Errors

Returns LeanWorkerError under the same conditions as Self::infer_type. Lean-side failures surface inside the returned LeanWorkerMetaResult.

pub fn describe( &mut self, name: &str, cancellation: Option<&LeanWorkerCancellationToken>, progress: Option<&dyn LeanWorkerProgressSink>, ) -> Result<Option<LeanWorkerDeclarationRow>, LeanWorkerError>

Describe a declaration: its kind, rendered type, and source range.

Returns Ok(None) when the name is not in the session’s open environment.

Errors

Returns LeanWorkerError if the worker is dead, the child reports a host error, cancellation is observed, a progress sink panics, or protocol communication fails.

pub fn search_declarations( &mut self, search: &LeanWorkerDeclarationSearch, cancellation: Option<&LeanWorkerCancellationToken>, progress: Option<&dyn LeanWorkerProgressSink>, ) -> Result<LeanWorkerDeclarationSearchResult, LeanWorkerError>

Search declarations and return bounded metadata-only rows plus facts.

The worker applies structured name, kind, required-constant, conclusion-head, and scope filters inside Lean while scanning the imported environment. Rows are capped by search.limit (clamped to 1..=100 in the child) and contain no type signatures; use Self::declaration_type for explicit one-name type rendering.

Errors

Returns LeanWorkerError under the same conditions as Self::describe.

pub fn declaration_type( &mut self, name: &str, max_bytes: usize, cancellation: Option<&LeanWorkerCancellationToken>, progress: Option<&dyn LeanWorkerProgressSink>, ) -> Result<Option<LeanWorkerDeclarationType>, LeanWorkerError>

Render one declaration type under a byte cap.

The returned type text is never longer than max_bytes, except that the worker also applies a 64 KiB upper ceiling. Passing 0 requests an empty truncated rendering.

Errors

Returns LeanWorkerError under the same conditions as Self::describe.

pub fn inspect_declaration( &mut self, request: &LeanWorkerDeclarationInspectionRequest, cancellation: Option<&LeanWorkerCancellationToken>, progress: Option<&dyn LeanWorkerProgressSink>, ) -> Result<LeanWorkerDeclarationInspectionResult, LeanWorkerError>

Inspect one selected declaration under explicit output budgets.

Declaration search intentionally returns metadata-only rows. Use this method after selecting one declaration name whose rendered statement and docstring are worth paying for.

Errors

Returns LeanWorkerError under the same conditions as Self::describe.

pub fn attempt_proof( &mut self, request: &LeanWorkerProofAttemptRequest, options: &LeanWorkerElabOptions, cancellation: Option<&LeanWorkerCancellationToken>, progress: Option<&dyn LeanWorkerProgressSink>, ) -> Result<LeanWorkerProofAttemptResult, LeanWorkerError>

Try proof snippets against an in-memory source overlay.

The worker never writes source files. Each candidate returns a normal status row, including failed proofs and budget exhaustion.

Errors

Returns LeanWorkerError under the same conditions as Self::process_module_query_batch.

pub fn verify_declaration( &mut self, request: &LeanWorkerDeclarationVerificationRequest, options: &LeanWorkerElabOptions, cancellation: Option<&LeanWorkerCancellationToken>, progress: Option<&dyn LeanWorkerProgressSink>, ) -> Result<LeanWorkerDeclarationVerificationResult, LeanWorkerError>

Verify one declaration in an in-memory source snapshot.

Policy failures, missing declarations, and unsupported shim support are returned as structured result statuses rather than worker errors.

Errors

Returns LeanWorkerError under the same conditions as Self::process_module_query_batch.

pub fn verify_declaration_batch( &mut self, request: &LeanWorkerDeclarationVerificationBatchRequest, options: &LeanWorkerElabOptions, cancellation: Option<&LeanWorkerCancellationToken>, progress: Option<&dyn LeanWorkerProgressSink>, ) -> Result<LeanWorkerDeclarationVerificationBatchResult, LeanWorkerError>

Verify several declarations in one in-memory source snapshot.

The whole batch is one worker request for lifecycle, timeout, and progress purposes. Header/import state is returned once at the batch level; rows preserve the input target order.

Errors

Returns LeanWorkerError under the same conditions as Self::verify_declaration.

pub fn list_declarations_strings( &mut self, filter: &LeanWorkerDeclarationFilter, cancellation: Option<&LeanWorkerCancellationToken>, progress: Option<&dyn LeanWorkerProgressSink>, ) -> Result<Vec<String>, LeanWorkerError>

Enumerate the session’s open environment and return the matching declaration names as dotted strings.

The child streams names one per protocol frame so total payload size is unbounded; any single Lean name fits well under the per-frame cap.

Errors

Returns LeanWorkerError under the same conditions as Self::describe.

pub fn describe_bulk( &mut self, names: &[&str], cancellation: Option<&LeanWorkerCancellationToken>, progress: Option<&dyn LeanWorkerProgressSink>, ) -> Result<Vec<LeanWorkerDeclarationRow>, LeanWorkerError>

Describe a batch of declarations in one IPC round-trip.

Each input name produces one row in the returned vector, in the same order. Absent names keep their slot with kind == "missing", type_signature: None, and source: None so callers can correlate rows back to inputs positionally.

Errors

Returns LeanWorkerError under the same conditions as Self::describe.

pub fn process_module_query( &mut self, source: &str, query: LeanWorkerModuleQuery, options: &LeanWorkerElabOptions, cancellation: Option<&LeanWorkerCancellationToken>, progress: Option<&dyn LeanWorkerProgressSink>, ) -> Result<LeanWorkerModuleQueryOutcome, LeanWorkerError>

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

Errors

Returns LeanWorkerError if the worker is dead, the child reports a host error, cancellation is observed, a progress sink panics, or protocol communication fails. Header-parse failures, missing imports, and missing capability shims surface as variants of LeanWorkerModuleQueryOutcome.

pub fn process_module_query_batch( &mut self, source: &str, selectors: &[LeanWorkerModuleQuerySelector], budgets: &LeanWorkerOutputBudgets, options: &LeanWorkerElabOptions, cancellation: Option<&LeanWorkerCancellationToken>, progress: Option<&dyn LeanWorkerProgressSink>, ) -> Result<LeanWorkerModuleQueryBatchOutcome, LeanWorkerError>

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

Errors

Returns LeanWorkerError if the worker is dead, the child reports a host error, cancellation is observed, a progress sink panics, or protocol communication fails. Header-parse failures, missing imports, selector unavailability, budget exhaustion, and missing capability shims surface in the returned LeanWorkerModuleQueryBatchOutcome.

pub fn clear_module_snapshot_cache( &mut self, cancellation: Option<&LeanWorkerCancellationToken>, progress: Option<&dyn LeanWorkerProgressSink>, ) -> Result<LeanWorkerModuleSnapshotCacheClearResult, LeanWorkerError>

Clear the worker child’s private module snapshot cache.

Errors

Returns LeanWorkerError if the worker is dead, no session is open, cancellation is observed, or protocol communication fails.

pub fn run_data_stream( &mut self, export: &str, request: &Value, rows: &dyn LeanWorkerDataSink, diagnostics: Option<&dyn LeanWorkerDiagnosticSink>, cancellation: Option<&LeanWorkerCancellationToken>, progress: Option<&dyn LeanWorkerProgressSink>, ) -> Result<LeanWorkerStreamSummary, LeanWorkerError>

Run a downstream streaming export and deliver JSON rows to rows.

The Lean export must have ABI String -> USize -> USize -> IO UInt8. The child supplies the callback handle and trampoline; the parent only sees validated LeanWorkerDataRow values. Rows are delivered immediately and become committed only if this method returns terminal success.

Errors

Returns LeanWorkerError if the worker is dead, the child reports a host or stream error, cancellation is observed, a sink panics, or protocol communication fails. In-flight cancellation cycles the child and invalidates this session.

pub fn run_json_command<Req, Resp>( &mut self, command: &LeanWorkerJsonCommand<Req, Resp>, request: &Req, cancellation: Option<&LeanWorkerCancellationToken>, progress: Option<&dyn LeanWorkerProgressSink>, ) -> Result<Resp, LeanWorkerError>

where Req: Serialize, Resp: DeserializeOwned,

Run a typed non-streaming downstream JSON command.

The Lean export must have ABI String -> IO String. The request is serialized from Req; the returned JSON string is decoded into Resp. Use this for commands that return one terminal JSON value and no rows.

Errors

Returns LeanWorkerError if request encoding fails, the worker is dead, the session was invalidated, the export is missing, response decoding fails, cancellation or timeout is observed, a progress sink panics, or protocol communication fails.

pub fn run_streaming_command<Req, Row, Summary>( &mut self, command: &LeanWorkerStreamingCommand<Req, Row, Summary>, request: &Req, rows: &dyn LeanWorkerTypedDataSink<Row>, diagnostics: Option<&dyn LeanWorkerDiagnosticSink>, cancellation: Option<&LeanWorkerCancellationToken>, progress: Option<&dyn LeanWorkerProgressSink>, ) -> Result<LeanWorkerTypedStreamSummary<Summary>, LeanWorkerError>

where Req: Serialize, Row: DeserializeOwned, Summary: DeserializeOwned,

Run a typed downstream streaming command.

The Lean export must have ABI String -> USize -> USize -> IO UInt8. The request is serialized from Req; each row payload is decoded into Row; terminal metadata is decoded into Summary when present. Raw-row access remains available through run_data_stream. Rows are visible to rows immediately, but downstream callers that need atomic effects should commit them only after this method returns Ok.

Errors

Returns LeanWorkerError if request encoding fails, row or summary decoding fails, the worker is dead, the session was invalidated, the export fails, cancellation or timeout is observed, a sink panics, or protocol communication fails. Row decode errors include the stream and sequence that identified the bad payload.

pub fn capability_metadata( &mut self, export: &str, request: &Value, cancellation: Option<&LeanWorkerCancellationToken>, progress: Option<&dyn LeanWorkerProgressSink>, ) -> Result<LeanWorkerCapabilityMetadata, LeanWorkerError>

Query generic metadata from a downstream capability export.

The Lean export must have ABI String -> IO String. The request and response strings are JSON, but callers receive a typed metadata envelope rather than private protocol frames.

Errors

Returns LeanWorkerError if the worker is dead, the session was invalidated, the export is missing, request or response JSON is malformed, cancellation or timeout is observed, a progress sink panics, or protocol communication fails.

pub fn capability_doctor( &mut self, export: &str, request: &Value, cancellation: Option<&LeanWorkerCancellationToken>, progress: Option<&dyn LeanWorkerProgressSink>, ) -> Result<LeanWorkerDoctorReport, LeanWorkerError>

Run a generic doctor check from a downstream capability export.

The Lean export must have ABI String -> IO String. Doctor diagnostics are capability-layer facts; data rows remain reserved for downstream streaming payloads.

Errors

Returns LeanWorkerError if the worker is dead, the session was invalidated, the export is missing, request or response JSON is malformed, cancellation or timeout is observed, a progress sink panics, or protocol communication fails.