Crate lean_rs_worker 

Worker-process boundary for lean-rs host workloads.

LeanWorker is the public process-boundary supervisor. It hides child spawning, pipe management, protocol framing, child exit parsing, and cleanup behind a small lifecycle API. The protocol module is private; callers should not learn frame bytes or restart bookkeeping. LeanWorkerRestartPolicy cycles the child process for memory reset; it does not change the in-process lean-rs-host memory contract.

Structs

LeanWorker

Supervisor for one lean-rs-worker child process.

LeanWorkerBatchFingerprint

Stable cache-key-relevant facts for a planned batch.

LeanWorkerBootstrapCheck

One bounded worker bootstrap finding.

LeanWorkerBootstrapReport

Structured result of worker bootstrap checks for one capability builder.

LeanWorkerCancellationToken

Parent-side cancellation token for worker-session requests.

LeanWorkerCapability

A worker-backed capability with its Lake target built and worker started.

LeanWorkerCapabilityBuilder

Builder for a worker-backed Lean capability session.

LeanWorkerCapabilityFact

One named capability advertised by capability metadata.

LeanWorkerCapabilityMetadata

Generic metadata reported by one downstream capability package.

LeanWorkerChild

Locator for an app-owned worker child executable.

LeanWorkerCommandInfo

One top-level command projection. Mirrors lean_rs_host::process::CommandInfoNode.

LeanWorkerCommandMetadata

One downstream command advertised by capability metadata.

LeanWorkerConfig

Configuration for starting a lean-rs-worker child process.

LeanWorkerDataRow

One downstream-owned JSON row delivered over a worker request.

LeanWorkerDeclarationFilter

Filter applied when enumerating declarations from a session’s open environment.

LeanWorkerDeclarationRow

One declaration row returned by LeanWorkerSession::describe or LeanWorkerSession::describe_bulk.

LeanWorkerDiagnostic

One diagnostic emitted by worker elaboration, kernel checks, or MetaM services.

LeanWorkerDiagnosticEvent

One diagnostic message delivered over a worker request.

LeanWorkerDoctorDiagnostic

One structured capability health diagnostic.

LeanWorkerDoctorReport

Capability health report returned by a downstream doctor export.

LeanWorkerElabFailure

Diagnostic payload returned alongside meta and elaboration failures.

LeanWorkerElabOptions

Bounded elaboration options for worker-session requests.

LeanWorkerElabResult

Serializable elaboration result returned over the worker boundary.

LeanWorkerExit

Rendered child-process exit information.

LeanWorkerImportPlanConfig

Capability and session requirements used to plan worker batches.

LeanWorkerImportPlanner

Planner for worker-pool import/session batches.

LeanWorkerJsonCommand

A non-streaming downstream JSON command.

LeanWorkerKernelResult

Serializable kernel-check result returned over the worker boundary.

LeanWorkerKernelSummary

Projection of lean_rs_host::ProofSummary for the kernel-check success arm.

LeanWorkerModuleWork

One module-sized unit of planned worker work.

LeanWorkerNameRef

One identifier occurrence the elaborator recorded. is_binder distinguishes binding sites from use sites.

LeanWorkerPlanMetadataExpectation

Metadata expectation carried into planned session keys.

LeanWorkerPlannedBatch

One stable pool-execution batch.

LeanWorkerPool

Local pool for worker-backed capability sessions.

LeanWorkerPoolConfig

Configuration for a local LeanWorkerPool.

LeanWorkerPoolSnapshot

Summary of public pool state.

LeanWorkerProcessedFile

FFI-safe Elab.InfoTree projection. Mirrors lean_rs_host::process::ProcessedFile.

LeanWorkerProgressEvent

One progress event observed by the parent from a worker request.

LeanWorkerRendered

A Lean expression rendered to a string, together with the rendering path that produced it.

LeanWorkerRestartPolicy

Policy for cycling a worker child before the next request.

LeanWorkerRuntimeMetadata

Protocol/runtime facts reported by the worker child during handshake.

LeanWorkerSession

Narrow host-session adapter over a live LeanWorker.

LeanWorkerSessionConfig

Configuration for opening one host session inside a worker child.

LeanWorkerSessionKey

Worker reuse key for a capability-backed session.

LeanWorkerSessionLease

Borrowed lease for running typed commands on a compatible worker session.

LeanWorkerSourceRange

Source range Lean recorded for one declaration. Positions are 1-based.

LeanWorkerStats

Snapshot of worker lifecycle counters.

LeanWorkerStreamSummary

Summary returned after a worker data-stream export completes.

LeanWorkerStreamingCommand

A streaming downstream JSON command.

LeanWorkerTacticInfo

One tactic projection. Mirrors lean_rs_host::process::TacticInfoNode.

LeanWorkerTermInfo

One term projection. Mirrors lean_rs_host::process::TermInfoNode.

LeanWorkerTypedDataRow

One typed downstream row decoded from a worker data row.

LeanWorkerTypedStreamSummary

Typed summary returned after a streaming command reaches terminal success.

Enums

LeanWorkerBootstrapDiagnosticCode

Stable worker bootstrap diagnostic codes.

LeanWorkerBootstrapSeverity

Severity of one worker bootstrap finding.

LeanWorkerDoctorSeverity

Severity for a capability doctor diagnostic.

LeanWorkerError

Errors reported by the worker supervisor.

LeanWorkerImportPlanError

Import planning diagnostics.

LeanWorkerKernelStatus

Kernel-check status returned over the worker boundary.

LeanWorkerMetaResult

Outcome of one bounded MetaM service call over the worker boundary.

LeanWorkerMetaTransparency

Reducibility setting for is_def_eq, mirroring lean_rs_host::meta::LeanMetaTransparency.

LeanWorkerProcessFileOutcome

Outcome of LeanWorkerSession::process_file. Mirrors lean_rs_host::process::ProcessFileOutcome.

LeanWorkerProcessModuleOutcome

Outcome of LeanWorkerSession::process_module. Mirrors lean_rs_host::process::ProcessModuleOutcome.

LeanWorkerRendering

Which rendering path produced a LeanWorkerRendered::value.

LeanWorkerRestartPolicyClass

Coarse restart-policy class used in pool session keys.

LeanWorkerRestartReason

Reason recorded for the latest worker cycle.

LeanWorkerStatus

Public lifecycle state for a worker child.

Constants

LEAN_WORKER_REQUEST_TIMEOUT_DEFAULT

Default deadline for one worker request after startup.

LEAN_WORKER_REQUEST_TIMEOUT_LONG_RUNNING

Suggested deadline for long-running worker requests.

Traits

LeanWorkerDataSink

Parent-side sink for downstream data rows produced by one worker request.

LeanWorkerDiagnosticSink

Parent-side sink for diagnostics produced by one worker request.

LeanWorkerProgressSink

Parent-side sink for worker progress events.

LeanWorkerTypedDataSink

Parent-side sink for typed downstream data rows produced by one command.

Functions

run_worker_child_stdio

Run the worker child process on stdin/stdout.