Repository navigation
[v0.4] Certificates as kernel data tripled the non-Lean conformance suite on every host: run the stress arithmetic once, or make the data builders fast #177
Description
Measured on the v0.4 train (#167, head 0c206d983) against the last green main run (#166, run 39060792376), the build and non-Lean tests leg per host:
| host | before | on the train |
|---|---|---|
| aarch64-unknown-linux-gnu | 25 min | 59 min |
| aarch64-apple-darwin | 22 min | 74 min |
| x86_64-pc-windows-msvc | 41 min | 88 min |
| x86_64-apple-darwin | 51 min | cancelled at the 120-minute limit (run 39094595513) |
The conformance suite alone on the arm Linux runner: 1064 s to 3051 s (2.9 times). By the gaps between test completions on that leg (parallel threads, so approximate): conformance_sp_02 163 s to 1374 s; conformance_tc_05 60 to 307 s; conformance_sp_10 60 to 163 s; conformance_sp_12 about 124 s; conformance_sp_08 about 1600 s on a 4-core Linux box (the 9000-arm match derived as certificate B data, where the text derivation took under a minute).
Cause: with #157 (A) and #163 (B) the stress families and the wide match build their certificates as kernel terms, and the builders cost far more than the text generators they replace. What these cases check (lower bounds never above a certificate; a derivation independent of the stack depth) is platform-independent arithmetic, yet it runs on all four hosts of the matrix, whose purpose is that the compiler builds and its non-Lean behavior holds per platform.
#167 raises the host matrix's timeout-minutes to 300 (twice the slowest observed time, the rule its comment states) so a slow runner is not a false red. That bounds a hung job; it is not a fix. Two fixes, either or both, for the A/B lane (#89) and the CI lane:
- Run the stress arithmetic once: the certificate stress cases (
SP-02's families and mixed shapes,SP-08, andTC-05,SP-10,SP-12if they prove to be the ones) run whole on the normative host (thebdd-preservationleg, which already runs them) and on the other hosts run a small fixed slice that still exercises the builders on that platform. That is a SPEC §9.4 / §8.3 statement about what each host proves, and a register statement change where a case says "on every host". - Make the data builders fast: profile
data_aanddata_b/align.rson the 9000-arm match and the mixed shapes; the text generators were linear in the arms, and the kernel-term builders should be too.
Acceptance: the host legs back near their pre-train times (25 / 22 / 41 / 51 min) with no claim weakened; measured on one whole-gate run and recorded here.
Activity
afflom commentedon Oct 18, 2026
Measured on the train's whole-gate run 39101767733 (
f5748851c, 25 jobs, 730 runner-minutes, 102 min wall):build and non-Lean teststook 100 min on x86_64 macOS, 78 on arm macOS, 69 on Windows, 58 on arm Linux. The whole gate on #166's ready run was 516 runner-minutes, so this regression is about 210 runner-minutes per gate run and the wall time's critical path (the Intel macOS host;bdd-preservationis 93 min beside it). The host-matrixtimeout-minutesis 300 since0c206d983; it should come back down with the fix.Generated by Claude Code
Make kernel-term certificate data builders linear in match arms (#177)
afflom commentedon Oct 18, 2026
Whole-gate measurement on PR #189 (
838b47c6b, run 39122833578, 27/27 checks green withhost-matrixtimeout-minutes: 120restored), compared against the train's whole-gate run 39101767733 (f5748851c) and the initial #167 host-matrix run (90852ff07):90852ff07)39101767733)39122833578,838b47c6b)39101767733build and non-Lean tests (aarch64-unknown-linux-gnu)2h 44m(164m)58m 00s38m 45s(38.8m)build and non-Lean tests (aarch64-apple-darwin)2h 38m(158m)78m 00s45m 03s(45.0m)build and non-Lean tests (x86_64-pc-windows-msvc)2h 12m(132m)69m 00s46m 44s(46.7m)build and non-Lean tests (x86_64-apple-darwin)2h 38m(158m)100m 00s50m 51s(50.9m)just vv (bdd-preservation)(Lean-backed)93m 00s46m 35s(46.6m)host-matrixlegs +bdd-preservation)398.0 min228.0 min730.0 min596.4 minEvery
host-matrixleg is back at 39–51 minutes (≤ 50m 51son Intel macOS) with zero conformance tests or certificate checks removed or thinned.Make kernel-term certificate data builders linear in match arms (#177)
Wave 3: fast certificate data builders (#177), release follow-ups (#187…
afflom commentedon Oct 18, 2026
Acceptance measurement, on wave 3's whole-gate run 39145765325 (
7f2a00d35, #191, which carries #189's fix), against wave 2's run 39125361480 (the same tree plusBS-02, without the fix) and the pre-train times this issue names:aarch64-unknown-linux-gnuaarch64-apple-darwinx86_64-pc-windows-msvcx86_64-apple-darwinThe stress arithmetic is back near its pre-train cost:
bdd-preservation90 → 63 min,sp_021,707 s → (author's host) 129 s,tc_05740 → 53 s. What remains above the pre-train times on the hosts isBS-02's differential, whichcargo test --workspaceruns on every host (#190): about 30–50 minutes per host. The host matrixtimeout-minutesis 240 onmain(twice the slowest observed time, 140, per the comment's rule); with 104 as the new slowest, #190's fix is the next occasion to bring it down. No claim weakened: no test, assertion or certificate was thinned, and every record is byte-identical. Closing with the merge of #191.Generated by Claude Code