Keyboard shortcuts

Press or to navigate between chapters

Press S or / to search in the book

Press ? to show this help

Press Esc to hide this help

Lean-Dup Readiness Proof

A boundary check showing that the generic worker foundation can replace the subprocess-worker shape used by a lean-dup-class tool. The lean-rs-worker pool hosts the operational responsibilities; downstream crates keep their schemas and semantic policy. This is not a lean-dup implementation and not a migration guide.

What The Proof Covers

The readiness example runs:

cargo run -p lean-rs-worker --example lean_dup_readiness

The example uses the normal large-scale path:

LeanWorkerImportPlanner -> LeanWorkerPool -> LeanWorkerSessionLease -> typed command

It exercises six command shapes through generic typed commands:

  • version as a typed JSON command;
  • doctor as a typed JSON command;
  • extract as a typed streaming command;
  • features as a typed streaming command;
  • index as a typed streaming command;
  • probe as a typed streaming command.

The fixture exports use command-like names only to stress the worker capability layer. They do not define declaration rows, feature rows, probe results, cache keys, ranking, report policy, or source provenance for lean-dup.

Responsibility Map

Current subprocess responsibilitylean-rs-worker primitive
Start and supervise a Lean subprocessLeanWorkerPool and worker supervisors
Build/load the worker capabilityLeanWorkerCapabilityBuilder plus lean-toolchain
Batch modules by import/session requirementsLeanWorkerImportPlanner planned batches
Reuse imported sessionsLeanWorkerSessionLease keyed by session material
Stream JSONL-like rowstyped worker streaming commands and data sinks
Separate diagnostics from dataLeanWorkerDiagnosticSink
Emit progress/control eventsLeanWorkerProgressSink
Mark output committableterminal summaries with commit-after-success semantics
Enforce request deadlinesrequest timeout/watchdog policy
Recover from child panic/aborttyped child-failure errors and fresh leases
Reset Lean process-global memoryexplicit/policy worker cycling
Observe large runsLeanWorkerPoolSnapshot and lease snapshots
Bound slow sinksbounded row-delivery backpressure

This deletes caller-owned subprocess plumbing: ad hoc child spawning, stdin JSON request writing, stdout JSONL framing, stderr parsing, EOF classification, manual timeout kills, manual restart sequencing, pipe-draining loops, and RSS/pool bookkeeping.

What Remains Downstream-Owned

A downstream project still owns:

  • request, row, and terminal summary schemas;
  • semantic algorithms for extraction, features, indexing, and probes;
  • cache validity and persistence;
  • ranking and reporting;
  • source provenance and user-facing paths;
  • command names and CLI policy;
  • any compatibility decisions based on downstream metadata.

This is the intended split. lean-rs-worker carries typed commands, rows, diagnostics, terminal summaries, timeouts, cycling, backpressure, and pool state; it does not know what a downstream row means.

Comparison Input

A read-only downstream checkout (e.g., a lean-dup clone) can be supplied via the LEAN_RS_LEAN_DUP_ROOT environment variable. The readiness example records the checkout revision when the path is set and points to a git repository. If LEAN_RS_WORKER_COMPARE_COMMAND is also set, the example runs that command and prints its status and elapsed time. The comparison is optional because lean-rs-worker should not depend on a local downstream checkout.

Any comparison must name the command, revision, workload, and limits. Without that, the readiness proof only claims generic coverage and local worker-pool operating behavior.

Measured Local Envelope

The example prints:

  • command-shape coverage and row counts;
  • diagnostic and progress counts;
  • terminal summary command names;
  • timeout, cancellation, fatal-exit recovery, explicit cycle, and backpressure outcomes;
  • pool snapshot counters;
  • parent and child RSS when the platform permits sampling;
  • optional subprocess comparison status.

Do not treat the fixture rows as lean-dup rows. They are small generic test data used to prove that the worker substrate can carry the shape.