Expand description
What survives a command’s output, decided by which command produced
it. compaction reads the shape of a text; this reads the identity
of its author, because cargo build and git status are both logs
and their noise has nothing in common.
The replay path never calls a model. The same seed must replay a
byte-identical window (ARCHITECTURE.md §10), and a compactor that
thinks cannot be replayed. A first run may ask an adviser, and its
answer is a recorded fact (adviser_asked, adviser_answered,
adviser_fell_back) rather than something this module recomputes —
which is why no adviser appears in the stage chain below.
Seven stages run in a fixed order, each accepted only when it shrank the text, and every stage that ran — applied, no-op, refused or unavailable — is carried in the answer: a cut’s account, or a pass’s account. Below the floor no stage runs at all and the reason is the account.
The tee comes first and is not optional. The original is pinned in
the CAS and materialized as a rest file before anything is cut,
which is why this may cut harder than a compactor that cannot
promise the way back. Parameters are crates/runtime/spec/Sieve.lean §8-27-5, and are
not choices to revisit here.
Re-exports§
pub use diff::SieveHistory;pub use filter::Filter;pub use filter::FilterTable;pub use key::CommandKey;pub use record::PassReason;pub use record::ResultOffloaded;pub use record::SieveAccount;pub use record::SieveRecord;pub use record::Sieved;pub use record::Stage;pub use record::StageOutcome;pub use record::StageReport;
Modules§
- diff
- What this run already saw from the same command, and only what
changed since.
cargo checkrun ten times in a development loop prints nine outputs that are mostly the previous one; the model is better served by “this error is new” than by reading both. - filter
- The filter table: what
FILTERS.tomlmay say, the three reducers compiled in, and which entry a command key hits. - key
- Which command produced an output. The identity a filter matches
and the differencing groups by: the arm, the program, its
arguments. Ordered so it can key a
BTreeMap, never a hash. - record
- What the sieve answers with: the text the model sees, the way back to the original, and the account of every stage — kept, no-op, refused, or unavailable — so a filter that stops working can be read off the Ledger afterwards. The payload holds integers and strings only.
Structs§
Constants§
- HEAD_
LINES - MAX_
TOTAL_ LINES - More lines than this and the middle is kept by priority.
- MIDDLE_
LINES - SIEVE_
FLOOR - Output at or below this passes untouched, without even a tee.
- TAIL_
LINES
Functions§
- sieve
- Sieves one command output. Order and parameters are the SPEC’s;
the tee runs before any stage, and the history is updated whether
or not anything was cut, so the next call can difference against
this one.
Passedcarries the input unchanged.