ci: cache Rust build + Verus, cancel superseded PR runs, fail-fast ordering - #5
Merged
Merged
Conversation
…dering Reduces CI wall-clock — which the --verify ci kickoff-agent loop blocks on for every iteration. No change to what is gated (R-DEFER-6 hard gate intact): - Swatinem/rust-cache@v2: caches cargo registry + git deps + workspace target dir (keyed on Cargo.lock + toolchain); turns the cold full-workspace compile into a warm incremental one. - actions/cache@v4 for the pinned Verus distribution (verus-0.2026.05.24...), downloaded+unzipped once instead of every run; install step is a no-op on a cache hit, falls back to download on a miss. - concurrency block with cancel-in-progress for pull_request events only (main pushes stay the verification record of record and are never cancelled). - fail-fast ordering: cargo fmt + the python doc-drift gates run before the Rust build cache restore and the heavy build/test/clippy, so a fmt slip or a stale design-doc pin fails in seconds, not after a multi-minute compile. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
maxine-at-forecast
force-pushed
the
feature/ci-cache-concurrency
branch
from
June 12, 2026 23:52
a7370fe to
545d80c
Compare
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
1 participant
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.
What
CI wall-clock optimization for
.github/workflows/ci.yml. No change to what is gated — the full gauntlet (build, test, clippy, fmt, skill-budget, doc-drift) still runs and still hard-fails on any non-zero exit (R-DEFER-6).Why now
Every
--verify cikickoff agent (the spike agents, and the many stage-1/stage-2 implementation agents to come) blocks on this CI and polls it with a bounded timeout. The repo had no caching of anything — each run cold-compiled all 7 workspace crates + deps + Verus-using test targets, and re-downloaded the pinned Verus zip. Shrinking that latency compounds across every agent iteration.Changes
Swatinem/rust-cache@v2— caches the cargo registry + git deps + workspacetarget/(keyed onCargo.lock+ toolchain). Cold full-workspace compile → warm incremental.actions/cache@v4for Verus — the pinnedverus-0.2026.05.24.ecee80adistribution is downloaded+unzipped once and cached by version; the install step is a no-op on a cache hit and falls back to download on a miss.concurrency+cancel-in-progress— superseded PR runs are cancelled when a new commit is pushed;mainpushes are never cancelled (those runs are the verification record of record).cargo fmt --checkand the two pythondoc-driftgates now run before the Rust build cache restore and the heavy build/test/clippy, so a formatting slip or a stale design-doc pin fails in seconds instead of after a multi-minute compile.Out of scope
A Lean CI job (umbrella REQ-2a) is the real coverage gap —
ci.ymlhas nolake build/#print axiomsstep, so Lean proofs aren't checked in CI. That's a separate, slower PR (needslake/Mathlib caching) and is deliberately not bundled with these zero/low-risk changes.🤖 Generated with Claude Code