Conversation
Windows-marker pattern generalized to every nix lane: the gate hashes all inputs the lanes consume (crate/lambda/template sources, lockfiles, toolchain, nix files, check script) and looks up per-lane nix-green-<lane>-<hash> markers via the caches API; green lanes mint them. A push that leaves the hash unchanged — hash-manifest records, workflow edits, docs — skips every already-green lane in seconds. Identical inputs imply an identical verdict (the checks are hermetic), so a marker minted by any branch is valid everywhere.
The workspace ships with fat LTO + codegen-units=1, and under --release every test binary pays that link. checkfast (inherits release, lto off, cgu 16) compiles the workspace test targets in 32s where release takes 157s (measured locally; 773/773 tests pass identically, run time unchanged at ~11s — verdicts are semantics, not codegen). nextest and lambda-tests build against a second cached deps closure under the new profile; clippy, abgen-all and every shipped artifact keep full-fat release. The cache composite gains a flavor input (nix-v4 keys) so the two closures never race for one entry.
The windows green marker was saved on windows-2025 but looked up from the linux gate: actions/cache versions an entry by (path, compression, OS flag), so without enableCrossOsArchive on both sides the marker was permanently invisible and the windows lane never skipped. Node addon had no marker at all. With both fixed, a push that touches no lane inputs (e.g. recording artifact hashes) skips every lane.
Member
Author
|
Measured, on this branch:
The windows marker was invisible by construction before 4c89e47: saved on windows-2025, looked up from linux, and actions/cache versions entries by (path, compression, cross-OS flag) — buildId rotated to |
The hashFiles allow-lists approximated each lane's input closure by hand; an omitted input meant a silent false-green skip (and ci.yml itself was already outside the nix lanes' set). Now: - nix lanes: marker key = sha256 of the lane's check drvPaths (nix eval, qemu binfmt for the arm IFD) + the harness files outside the drvs. Same key means same derivations; hermeticity means same verdict. This also subsumes the diff-based run_crate/run_lambda/run_lint path gates, which had the same allow-list failure mode — deleted. - windows/node lanes (no drvs): deny-list tree hash — every tracked file counts except a short justified exclusion list, so an omission there over-tests instead of under-testing. - ci/formal/MemoModel.v (rocq, compiles): drv_key_skip_sound, allowlist_false_green (constructive counterexample), denylist_skip_sound under the per-entry irrelevance hypothesis.
The drv-key gate spent ~6 min rebuilding 63 tiny IFD drvs (crane's Cargo.toml cleaning + dummy sources, the arm half under qemu) on every push. A 'gate' flavor of the binary cache persists them; the flavor key rotates only on manifest/lockfile/nix changes, so source-only pushes get an exact hit and the gate drops to eval time.
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
The two levers from the CI interview, measured and wired:
checkfast profile — the workspace ships with fat LTO + codegen-units=1, and under
--releaseevery test binary pays that link.checkfast(inherits release,lto off,cgu 16) compiles the workspace test targets in 32s where release takes 157s (4.9×), with 773/773 tests passing identically and run time unchanged (~11s) — verdicts are semantics, not codegen. nextest + lambda-tests now build against a second cached deps closure under the new profile; clippy, abgen-all, and every shipped artifact keep full-fat release. Predicted nix test lanes: ~14 min → ~4–6 min on free runners.Green-marker memoization — the windows-marker pattern generalized: the gate hashes every input the nix lanes consume and skips lanes already green for that hash (markers minted on green, looked up via the caches API — identical inputs ⇒ identical verdict, so a marker from any branch is valid everywhere). Hash-record pushes, workflow edits, and docs commits stop rebuilding anything.
Also: the cache composite gains a
flavorinput (nix-v4-keys) so the two deps closures never race for one entry. First run is cold (new keys + new closure); judge by the second.buildId rotates (Cargo.toml + nix/build.nix) — hash record to follow on this branch once CI is green.