Skip to main content

Module sieve

Module sieve 

Source
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 check run 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.toml may 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§

SieveInput

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. Passed carries the input unchanged.