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 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_file( &mut self, source: &str, options: &LeanWorkerElabOptions, cancellation: Option<&LeanWorkerCancellationToken>, progress: Option<&dyn LeanWorkerProgressSink>, ) -> Result<LeanWorkerProcessFileOutcome, LeanWorkerError>

Parse, elaborate, and project a Lean source string into an Elab.InfoTree projection. The session’s open environment supplies the imports; the source must not declare its own header.

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. Per-command elaboration failures appear inside LeanWorkerProcessedFile::diagnostics; the LeanWorkerProcessFileOutcome::Unsupported arm surfaces missing capability shims.

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

Parse a Lean module header (import declarations and prelude) and elaborate the body; project both into an Elab.InfoTree projection plus the parsed import list.

Errors

Returns LeanWorkerError under the same conditions as Self::process_file. Header-parse failures, missing imports, and missing capability shims surface as variants of LeanWorkerProcessModuleOutcome.

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.

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.

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.