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