Repository navigation
BS-02's differential runs on every host of the matrix and costs the gate about 140 runner-minutes #190
Description
Follow-up to #171 (wave 2, BS-02), measured on its gate run 39125361480 against the train's run 39101767733 on the same runners.
| Job | train (#167) | wave 2 (#171) |
|---|---|---|
| whole gate, runner-minutes | 730 | 872 |
| wall | 102 min | 158 min |
build and non-Lean tests (x86_64-apple-darwin) |
100 | 140 |
build and non-Lean tests (x86_64-pc-windows-msvc) |
69 | 105 |
build and non-Lean tests (aarch64-apple-darwin) |
78 | 87 |
build and non-Lean tests (aarch64-unknown-linux-gnu) |
58 | 66 |
just vv (bdd-production) |
27 | 43 |
just vv (bdd-compiler) |
15 | 30 |
just vv (rest) |
24 | 39 |
Why. BS-02's platform-independent part (support::lean_backed false) is the whole differential: the lowered lex and auditTokens under the calculus evaluator on 1,731 vectors and 300 seeded texts per root, then the rendered rust-std packages compiled by rustc and run on 5,731 inputs per root, then seven planted defects each re-lowered and re-evaluated. On the normative host it takes about 45 minutes (2,687 s with the Lean-backed export check). cargo test --workspace --all-features on each host of the matrix runs that part, so the four hosts each pay it, and the evaluator (an interpreter over the lowered program) dominates: the Intel mac now runs 140 of its 300-minute budget. bdd-production grew because the export certifies two more roots through Lean, which is BS-02's inherent cost. The growth of rest (24 → 39) after BS-01/BS-02 left it is not explained by this PR's changes and may be runner variance (bdd-verification fell 28 → 21 in the same run); one more run will say.
Proposal (not decided here):
- The evaluator half of the differential is platform-independent logic (the calculus evaluator and the Rust oracle are the same Rust on every host); the
rustchalf is the one that says something per host. SplitBS-02so the host matrix runs therustcdifferential on the vectors only, and the seeded corpora (300 evaluator texts, 4,000 rustc texts per root) and the seven plants run once, in thecompilerbdd part on the normative host. The register statement then names where each part runs (R2). - Or reduce the evaluator corpus: the 1,731 deterministic vectors already cover every branch the seven plants exercise; the 300 seeded texts per root are the slow part under the interpreter.
Either is a change to crates/conformance/src/cases/bootstrap.rs and the BS-02 statement, with no regeneration of records. BS-01 has the same shape at a smaller scale and would follow.
Related: #177 (the host matrix's own regression from the data-certificate stress tests).
Activity
afflom commentedon Oct 18, 2026
Measurements from PR #189 rebased onto
mainafter wave 2 (eff2cd382, run 39138077085) confirm that once #177's fast certificate data builders are in,conformance_bs_02is the sole long-pole tail on everyhost-matrixleg:conformance.rsstartsconformance_bs_02finishesconformance_bs_02wall timeaarch64-unknown-linux-gnu(job)sp_02)aarch64-apple-darwin(job)tc_05)x86_64-pc-windows-msvc(job)tc_03)x86_64-apple-darwin(job)tc_03)For comparison,
conformance_bs_01took 2.4m onx86_64-pc-windows-msvc, 2.9m onaarch64-unknown-linux-gnu, 4.4m onaarch64-apple-darwin, and 6.7m onx86_64-apple-darwin.On Proposal 1 vs. Proposal 2:
BS-02andBS-01viasupport::normative_host()orsupport::lean_backedso the host matrix runs therustcdifferential on the deterministic vectors while the evaluator differential, the seeded corpora, and the 7 planted defects run once on the normative host inbdd-compiler), each non-normative host still checks that the renderedrust-stdpackages compile under that host'srustcand agree with the Rust oracle on every deterministic vector (the part that actually varies by host/target), while the platform-independent interpreter and mutation loop run once onx86_64-unknown-linux-gnu.conformance_bs_02onx86_64-apple-darwinfrom >97m to ~1–2m (rustcbuild + vector binary execution), bringing the Intel macOS leg down to ~82m (its 16:35:50Z completion of the other 413 tests) and restoring the 120-minutehost-matrixtimeout with ~38 minutes of margin.@afflom if Proposal 1 looks right to you, we can open a focused draft PR for #190 (touching only
crates/conformance/src/cases/bootstrap.rsand theBS-01/BS-02wording inSPEC.md, with zero record or artifact movement).Wave 3: fast certificate data builders (#177), release follow-ups (#187…
afflom commentedon Oct 18, 2026
Opened PR #192 (
db6a9439f, rebased on Wave 3mainefea57d85) implementing Proposal 1 and restoring thehost-matrixtimeout-minutesto120:39145765325),x86_64-apple-darwinfinished all other 413 conformance tests at17:53:27Z(60.3m intoconformance.rs), whileconformance_bs_02ran until18:21:08Z(83.5m total, adding 27.7m of tail after every other test had finished).host-matrixstill checks and buildsbootstrap/, renders therust-stdpackages forisClosedLeanName,parseAuditOutput,lex, andauditTokens, compiles them with that host's pinnedrustc, and runs the compiled binaries on the deterministic vector corpora (audit_vectors(),name_vectors(), and the 1,731token_vectors()), while the platform-independent calculus evaluator differential, the seeded corpora, the 14 planted defects, and the Lean production export run once on the normative host (just vv (bdd-compiler)).BS-01andBS-02inSPEC.md§17.23,model/ids.toml,CONFORMANCE.md, andfeatures/suites/bootstrap.feature(R2), with zero record or artifact movement.Full gate run (
39154991151) is running now on PR #192 to measure the newhost-matrixtimes. cc @afflom @humuhumu33