explanationView source

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.