Repository navigation
ci: Evidence Refresh proves in parallel shards (Fixes #4744) - #4774
Merged
Merged
Conversation
The det sweep (4 shards) and the stale-record re-proofs (6 shards) run as parallel jobs of one pinned commit; a short refresh job merges them (proof_sweep.py --aggregate --skip-ledger-check, evidence.py --shard), rewrites the ledger, re-renders the pages and opens the bot PR. Same proofs, ratchet, lanes, Db2 job and auto-merge/failure rules. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01MQNoe4wPJgr7dbUvs3DG6D
Contributor
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.
Fixes #4744.
Measured (runs 37859714260, 37866635888; one 4-vCPU runner, sequential)
det sweep 2111-2753 s, stale-record re-proofs 2002-2579 s (41 records, ~55 s each), checkout ~50 s, report ~40 s: 75-100 min.
Design
lanepins main's head once (shaoutput); every job checks out that commit, so parallel jobs are of the same tree (the Db2 job andrefreshuse it too).sweep: 4 shards ofproof_sweep.py --det-only --skip-db2 --shard I/4 --no-ratchet(balanced by det_sweep_durations.json, as det-sweep.yml).records: 6 shards ofevidence.py refresh --stale --skip-db2 --shard I/6(new flag: every shard computes the same stale list and takes every 6th; tested that the slices are exactly the unsharded selection). Each stages the records it wrote.refresh(slimmer: no JDK/Maven/oracle image, the proof shards still check the oracle pin strictly): downloads both, copies the records in (onlyevidence.jsonregular files),evidence.py render,proof_sweep.py --aggregate ... --expect all --skip-ledger-check(new flag; the ledger is rewritten from this sweep next, as before), ledger update, report rebuild, PR.Preserved
Push/full lanes and concurrency groups (#4745), Db2 job and its handling (#4740), stale-level handling (#4734/#4761), auto-merge retry (#4757). A failed proof (records shard fails, staged anyway), a failed/missing sweep shard (aggregate names missing cases), a failed ratchet or Db2 job: PR opened, no auto-merge, run fails.
Estimate
~5 min setup + slowest shard (sweep ~11 min, records ~7 min) + ~8 min refresh = ~25 min (was 75-100).
Not done
Skipping re-proofs an open bot PR already carries (needs PR-content comparison; follow-up). Verified: actionlint and zizmor clean,
pr_gates.py --fast5/5, new unit tests. The workflow itself can only be exercised on main.Post-merge verification
Dispatch
Evidence Refreshwith db2=false and keys=one record (checks the graph), then a push-lane run and compare job times with the above; confirm the bot PR diff matches an unsharded run's.🤖 Generated with Claude Code
https://claude.ai/code/session_01MQNoe4wPJgr7dbUvs3DG6D