The incremental engine#
What is cached, and what it is keyed by#
The unit is a module's Checked Interface: a header, a lazily decoded body, a semantic digest that excludes the source digest, and an integrity digest.
An entry is usable only when all of these match:
- the module's source digest;
- its base position in the shared context;
- every dependency's interface digest;
- the compiler identity;
- the edition;
- the interface schema version.
Any mismatch is a miss. There is no timestamp anywhere in the key: two checkouts with the same bytes hit the same entries.
Why a comment edit is cheap and a literal edit is not#
A module's semantic digest ignores its source digest. Editing a comment changes the module's source digest — so that module re-checks — but its interface digest is unchanged, so nothing below it moves. Changing a literal changes the interface digest, and every dependent's key changes with it.
Measured on the application closure: a comment-only edit re-checks 1 module in about 165 ms; a semantic edit to a base module re-checks the cone in 7.3 s.
The cache-trust boundary#
Re-admitting a cached interface means trusting kernel-checked data without
re-running the kernel. That is allowed only through validation: schema,
lengths, key and digests are checked first, and a corrupt body aborts before
the context is used. debug/security-check.py corrupts entries on purpose: a
truncated entry is detected, and a poisoned entry cannot change the artifact.
Writes are atomic, cancellation is clean#
Entries are written to a temporary name and renamed into place, so an interrupted run leaves unpromoted candidates rather than half-written entries, and the next run sweeps them. After a SIGINT mid-check the suite finds zero stray temporaries and the next run completes.
Performance history#
The warm no-change path went 29 s → 0.17 s through eight profile-driven steps. The largest were: a quadratic list decoder replaced by a ByteString-indexed one; strict checksum folds; not forcing interface bodies to count definitions; and adopting a sealed program lazily.
The budgets live in docs/baseline/compiler-budgets.txt: among them a warm
no-change check within 1 s, a leaf declaration edit within 2 s, a proof-heavy
affected cone within 10 s and a clean conformance check within 60 s.
alpha bench compiler measures this workspace against them, and --gate
exits 1 on a miss.
Parallelism, and what is not built#
--jobs N parses up to N modules at once, deterministically; checking itself
stays sequential, and a budgeted run with --jobs greater than one accepts
only a wall-time budget. Watch mode reports check events, but retained-memory
and cache-ownership reporting are not built; the language-platform registry
(docs/baseline/language-platform-registry.json) records that as open rather
than implying it is done.