# lean-rs-worker
Worker-process boundary for `lean-rs` host workloads. Supervises a `lean-rs-worker-child` process around the in-process
theorem-prover stack in [`lean-rs-host`](https://docs.rs/lean-rs-host), adding fatal-exit containment, memory cycling,
request timeouts, and parent-owned row streaming.
Use this crate when a downstream tool needs process isolation, live rows, diagnostics, terminal summaries, request
timeouts, or memory cycling. Use `lean-rs-host` directly for trusted in-process work that does not need those
guarantees.
## Quick start in this repo
```sh
cargo run -p lean-rs-worker --example worker_capability_runner
```
The runner is the normal downstream shape: `LeanWorkerCapabilityBuilder` manages startup, typed commands carry requests
and rows, diagnostics arrive on a separate sink, and explicit cycling resets process-global memory. The full recipe is
[`docs/recipes/worker-capability-runner.md`](https://github.com/jcreinhold/lean-rs/blob/main/docs/recipes/worker-capability-runner.md).
This in-tree example uses the workspace worker child. It is useful for learning the API and for testing `lean-rs-worker`
itself.
## Ship your own worker app
For a shipped application, build the Lean capability in `build.rs` with `lean_toolchain::CargoLeanCapability`, embed the
resulting path with `lean_rs::LeanBuiltCapability::manifest_path(env!(...))`, and ship an app-owned worker child binary:
```rust,ignore
fn main() -> std::process::ExitCode {
lean_rs_worker::run_worker_child_stdio()
}
```
Point the builder at that binary with
`LeanWorkerChild::sibling("my_app_lean_worker").env_override("MY_APP_LEAN_WORKER")`. Run
`LeanWorkerCapabilityBuilder::check()` in installers, startup probes, or doctor commands to validate the child binary,
manifest-backed capability, protocol handshake, import session, and optional metadata expectation before real work
starts. This is the production packaging path because Cargo does not install dependency binaries as part of your
application. See
[`docs/recipes/ship-crate-with-lean.md`](https://github.com/jcreinhold/lean-rs/blob/main/docs/recipes/ship-crate-with-lean.md).
## What the crate owns
| Child process lifecycle, pipes, frame decoding, fatal-exit classification, cleanup | `LeanWorker`, `LeanWorkerConfig`, `LeanWorkerError`, `LeanWorkerExit`, `LeanWorkerStats` |
| Restart and memory-cycling policy: explicit cycling, request-count threshold, import-like threshold, idle interval, RSS ceiling | `LeanWorkerRestartPolicy`, `LeanWorkerRestartReason` |
| Capability startup: Lake build or manifest-backed artifact use, child resolution, bootstrap check, health-check, import session, optional metadata validation | `LeanWorkerCapabilityBuilder`, `LeanWorkerBootstrapReport` |
| Packaged worker child resolution | `LeanWorkerChild`, `run_worker_child_stdio` |
| Typed downstream commands and row streams | `LeanWorkerJsonCommand<Req, Resp>`, `LeanWorkerStreamingCommand<Req, Row, Summary>`, `LeanWorkerTypedDataSink`, `LeanWorkerDiagnosticSink` |
| Narrow host-session adapter (elaboration, kernel-check status, declaration-kind/name bulk queries) | `LeanWorker::open_session` |
| Local multi-worker fanout, warm reuse, fixed admission, RSS-aware policy, lease invalidation | `LeanWorkerPool`, `LeanWorkerSessionLease`, `LeanWorkerSessionKey`, `LeanWorkerPoolSnapshot` |
| Import planning: Lake module discovery to stable pool-execution batches | `LeanWorkerImportPlanner`, `LeanWorkerPlannedBatch` |
| Progress and cancellation across the IPC boundary | `LeanWorkerProgressEvent`, `LeanWorkerError::Cancelled` |
## What the crate does not own
- Downstream command names, request schemas, row schemas, summary schemas.
- Cache validity, ranking, reporting, source provenance, CLI policy.
- Child PIDs, worker IDs, pipes, protocol frames, or which warm worker the pool selected.
- Remote (cross-host) workers, byte callbacks, object callbacks. These are non-goals for the current local-scale
release; see
[`docs/architecture/28-production-scale-release.md`](https://github.com/jcreinhold/lean-rs/blob/main/docs/architecture/28-production-scale-release.md).
## Key behaviors
**Cycling is the reset boundary for Lean process-global memory.** A `LeanWorkerRestartPolicy` cycles the child before
requests when a configured request count, import-like request count, RSS ceiling, or idle duration is reached.
`SessionPool::drain()` is an in-process cache operation, not an RSS reset.
**Startup and request timeouts are independent.** Startup timeout covers the child handshake. Request timeout covers one
request after its frame is written, including live rows, diagnostics, progress, and terminal response. On
request-timeout expiry the supervisor kills and replaces the child, records `LeanWorkerRestartReason::RequestTimeout`,
returns `LeanWorkerError::Timeout`, and invalidates the open worker session.
**Row delivery uses bounded internal buffering.** Slow sinks block the request path instead of growing memory without
bound. Rows are never dropped for committed streams. Delivered rows are tentative until terminal success returns
`LeanWorkerTypedStreamSummary` with total rows, per-stream counts, elapsed time, and optional typed metadata.
**Large row streams use a raw-JSON payload fast path.** The child validates payload as JSON, the protocol carries it
without building a `serde_json::Value` tree, and typed commands deserialize directly into the caller row type at the
parent boundary. `LeanWorkerDataRow` remains the schema-less escape hatch when callers want arbitrary inspection rather
than maximum throughput.
**RSS sampling is best-effort and platform-specific.** Unavailable samples are recorded as unavailable, not as a false
claim that the pool is under budget.
**Capability metadata and doctor checks are separate from row streams.** `LeanWorker::runtime_metadata` reports protocol
facts from the child handshake. `LeanWorkerSession::capability_metadata` and `LeanWorkerSession::capability_doctor` call
downstream exports with ABI `String -> IO String`, decode the returned JSON into generic command, capability, version,
and diagnostic envelopes, and leave cache policy and semantic command meaning to the downstream tool.
## Lean-side helpers
Lean capability packages should use `LeanRsInterop.Worker.Stream` from `lean-rs-interop-shims` when emitting worker
streams. The helpers build row, diagnostic, progress, terminal-metadata, and status envelopes for the child-local string
callback path. They do not define downstream row schemas, command names, session keys, or pool scheduling policy.
## More examples
| `cargo run -p lean-rs-worker --example worker_streaming` | Typed streaming command with parent-side watchdog and worker cycling. |
| `cargo run --release -p lean-rs-worker --example worker_capability_probe` | Operational probe over generic command shapes (`version`, `doctor`, `extract`, `features`, `index`, `probe`); records cold startup, first import, cancellation latency, fatal-exit recovery, cycling, throughput, RSS. Set `LEAN_RS_WORKER_COMPARE_COMMAND=…` to time a comparison command alongside. |
| `cargo run -p lean-rs-worker --example worker_pool` | Pool, lease acquisition, typed streaming command, leased-worker cycling. |
| `cargo run -p lean-rs-worker --example pool_memory_scheduling` | Pool memory-aware admission and cycling under a small import policy. Records parent RSS, child RSS snapshots, unavailable samples, budget admission, policy restarts. |
| `cargo run -p lean-rs-worker --example mathlib_scale_probe` | Planner → pool → lease → typed command path. Set `LEAN_RS_MATHLIB_ROOT=/path/to/mathlib4` to use a real module list as planning workload. |
| `cargo run -p lean-rs-worker --example lean_dup_readiness` | Readiness fixture over all command shapes. Set `LEAN_RS_LEAN_DUP_ROOT=/path/to/checkout` to record the comparison checkout's revision; set `LEAN_RS_WORKER_COMPARE_COMMAND=…` to time a comparison command. |
The `mathlib_scale_probe` and `pool_memory_scheduling` examples need the worker child built first:
`cargo build -p lean-rs-worker --bin lean-rs-worker-child`.
## Recipes and contracts
- [`docs/recipes/worker-capability-runner.md`](https://github.com/jcreinhold/lean-rs/blob/main/docs/recipes/worker-capability-runner.md):
normal downstream path.
- [`docs/recipes/ship-crate-with-lean.md`](https://github.com/jcreinhold/lean-rs/blob/main/docs/recipes/ship-crate-with-lean.md):
canonical packaged app path with `build.rs`, runtime open helper, and app-owned worker child.
- [`docs/recipes/worker-process-boundary.md`](https://github.com/jcreinhold/lean-rs/blob/main/docs/recipes/worker-process-boundary.md):
lower-level process-boundary recipe.
- [`docs/architecture/28-production-scale-release.md`](https://github.com/jcreinhold/lean-rs/blob/main/docs/architecture/28-production-scale-release.md):
local scale contract and non-goals.
## License
Dual-licensed under MIT or Apache-2.0 at your option.