Crate lean_rs_worker_parent

Expand description

Parent-side supervisor for the lean-rs worker process boundary.

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. Sessions, capability builders, and the local worker pool sit on top of it. The wire types it speaks come from lean_rs_worker_protocol and are re-exported on this crate’s public surface so callers do not need a second crate dependency for the common path.

This crate does not link libleanshared. The worker child runtime that does is published separately as lean-rs-worker-child.

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.
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.
LeanWorkerDeclarationFlags: Compact declaration flags returned by declaration search.
LeanWorkerDeclarationInspection: Bounded facts for one inspected declaration.
LeanWorkerDeclarationInspectionFields: Field selection for one declaration inspection request.
LeanWorkerDeclarationInspectionRequest: Bounded request to inspect one selected declaration.
LeanWorkerDeclarationOutlineResult: Result for LeanWorkerModuleQuerySelector::DeclarationOutline.
LeanWorkerDeclarationProofSearchFacts: Cheap proof-search facts for one declaration.
LeanWorkerDeclarationRow: One declaration row returned by LeanWorkerSession::describe or LeanWorkerSession::describe_bulk.
LeanWorkerDeclarationSearch: Bounded structured declaration search request.
LeanWorkerDeclarationSearchBias: Optional namespace/module preference for declaration search.
LeanWorkerDeclarationSearchFacts: Fanout and timing facts for a bounded declaration search.
LeanWorkerDeclarationSearchPruning: One broad fanout pruning record returned in search facts.
LeanWorkerDeclarationSearchResult: Result of a bounded declaration search.
LeanWorkerDeclarationSearchRow: One bounded metadata row returned by declaration search.
LeanWorkerDeclarationSearchTimings: Cheap elapsed timings for declaration search.
LeanWorkerDeclarationTargetInfo: Source metadata for the declaration surrounding a proof-agent query.
LeanWorkerDeclarationType: Bounded type rendering for a single declaration.
LeanWorkerDeclarationVerificationBatchItem: One target inside a batch declaration-verification request.
LeanWorkerDeclarationVerificationBatchRequest: Bounded request to verify several declarations in one in-memory source snapshot.
LeanWorkerDeclarationVerificationBatchRow: One ordered row inside a batch declaration-verification result.
LeanWorkerDeclarationVerificationFacts: Bounded facts returned by declaration verification.
LeanWorkerDeclarationVerificationRequest: Bounded request to verify one declaration in an in-memory source snapshot.
LeanWorkerDerivedWorkFacts: Observable derived work performed by one host query.
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.
LeanWorkerHostHandle: A worker-backed host session handle that is backed only by bundled shims.
LeanWorkerHostHandleBuilder: Builder for a worker-backed host session that loads only bundled shims.
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.
LeanWorkerLifecycleSnapshot: Compact lifecycle facts for callers that supervise a worker boundary.
LeanWorkerLocalInfo: One local declaration in a proof-state result.
LeanWorkerModuleCacheLimits: Typed limits for the worker child’s module snapshot cache.
LeanWorkerModuleQueryBatchEnvelope: Successful batch selector envelope.
LeanWorkerModuleQueryCacheFacts: Cache and timing facts attached to a batched module query outcome.
LeanWorkerModuleQueryTimings: Phase timings for a batched module query, measured in the worker child.
LeanWorkerModuleSnapshotCacheClearResult: Result of manually clearing the worker-side module snapshot cache.
LeanWorkerModuleSourceSpan: Source span in the original file. Positions are 1-based.
LeanWorkerModuleWork: One module-sized unit of planned worker work.
LeanWorkerNameRef: One identifier occurrence the elaborator recorded. is_binder distinguishes binding sites from use sites.
LeanWorkerOutputBudgets: Explicit byte budgets for batched module projections.
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.
LeanWorkerProgressEvent: One progress event observed by the parent from a worker request.
LeanWorkerProofAttemptEnvelope: Envelope for a bounded proof attempt.
LeanWorkerProofAttemptRequest: Bounded request to try one or more proof snippets without writing files.
LeanWorkerProofAttemptRow: Per-candidate proof attempt result row.
LeanWorkerProofCandidate: One proof candidate to apply to an in-memory source overlay.
LeanWorkerProofPositionSummary: Informational summary of the selected proof position. It is not an edit handle and cannot be fed back into proof-action requests.
LeanWorkerProofStateInfo: Proof-state payload for one cursor.
LeanWorkerReferencesResult: Result for LeanWorkerModuleQuery::References.
LeanWorkerRendered: A Lean expression rendered to a string, together with the rendering path that produced it.
LeanWorkerRenderedInfo: Bounded rendered Lean text.
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.
LeanWorkerShutdownReport: Structured result of shutting down a worker child.
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.
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.
LeanWorkerDeclarationInspectionResult: Outcome of inspecting one selected declaration.
LeanWorkerDeclarationNameMatch: Name-fragment matching policy for declaration search.
LeanWorkerDeclarationSearchScope: Scope kind used by declaration-search ranking bias.
LeanWorkerDeclarationTargetResult: Result for LeanWorkerModuleQuerySelector::DeclarationTarget.
LeanWorkerDeclarationVerificationBatchResult: Header-aware batch declaration-verification outcome.
LeanWorkerDeclarationVerificationResult: Header-aware declaration verification outcome.
LeanWorkerDeclarationVerificationStatus: Verification policy result after diagnostics and declaration facts are collected.
LeanWorkerDeclarationVerificationTarget: Target declaration for verification.
LeanWorkerDoctorSeverity: Severity for a capability doctor diagnostic.
LeanWorkerError: Errors reported by the worker supervisor.
LeanWorkerGoalAtResult: Result for LeanWorkerModuleQuery::GoalAt.
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.
LeanWorkerModuleCacheStatus: Worker-side module snapshot cache status for a batched module query.
LeanWorkerModuleQuery: Query shape for one header-aware Lean module processing request.
LeanWorkerModuleQueryBatchItem: One selector result in a batched module query.
LeanWorkerModuleQueryBatchOutcome: Outcome of LeanWorkerSession::process_module_query_batch.
LeanWorkerModuleQueryBatchResult: Typed payload returned by one successful batch selector.
LeanWorkerModuleQueryOutcome: Outcome of LeanWorkerSession::process_module_query.
LeanWorkerModuleQueryResult: Typed payload returned by a successful module query.
LeanWorkerModuleQuerySelector: One selector in a batched module-processing request.
LeanWorkerProofAttemptResult: Header-aware proof attempt outcome.
LeanWorkerProofAttemptStatus: Per-candidate proof attempt status.
LeanWorkerProofEditTarget: Target for a non-mutating proof attempt over an in-memory source overlay.
LeanWorkerProofPositionSelector: Intent selector for one proof position inside a declaration.
LeanWorkerProofStateResult: Result for LeanWorkerModuleQuerySelector::ProofState.
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.
LeanWorkerSessionImportProfile: Closed full-session import profiles understood by worker children.
LeanWorkerShutdownOutcome: Shutdown path used to reach a terminal child state.
LeanWorkerSorryPolicy: Policy for sorry-like constructs in declaration verification.
LeanWorkerSourceCoordinateSpace: Coordinate space a diagnostic position was reported in.
LeanWorkerStatus: Public lifecycle state for a worker child.
LeanWorkerSurroundingDeclarationResult: Result for LeanWorkerModuleQuerySelector::SurroundingDeclaration.
LeanWorkerTypeAtResult: Result for LeanWorkerModuleQuery::TypeAt.

Constants§

LEAN_WORKER_KILL_WAIT_TIMEOUT_DEFAULT: Default deadline for waiting on a killed child process to be reaped.
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.
LEAN_WORKER_SHUTDOWN_TIMEOUT_DEFAULT: Default deadline for graceful child shutdown before kill escalation.

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.