Repository navigation
Restructure CI: comparator battery at one pin, per-suite and per-pin jobs, parallel compiles - #71
Merged
Merged
Conversation
Comparator's verdict logic and the checker's staging do not vary with the FC pin, so test_proof_acceptance, test_lean_vuln_e2e and test_comparator_security now run once, at the OEIS pin (conftest's pin fixture). What does vary per pin -- toolchain, Mathlib, util-module layout, the cache-get permissions that bit in #65, the exporter built at that toolchain -- is covered by the new tests/test_pin_smoke.py (honest proof and honest disproof accepted in each pin's production images) plus test_comparator_primitives, both parametrized over apn.dataset.FC_PINS from Python via the every_pin fixture, so a new pin is tested without a CI change. The comparator job drops from 148 tests to 34; the per-pin work moves to a pin-smoke job.
…ry job The isolation job ran five datasets back to back, each building its own generate image; they are now one job each so the run's wall-clock is the slowest suite rather than the sum. The new all-checks job needs every other job and fails unless all of them succeeded (matrix suites included), so branch protection can require that one status. Suites are still selected by listing modules per job, with the tests job selecting by --ignore only: a module listed nowhere runs there, so forgetting to update this file cannot drop a suite from CI.
…ison The oracle re-extracted the 38 published gold proofs to compare each target_theorem_0 type with our spec's target, and the extractor elaborates the full proofs to do it: 384 s and 610 s in the two isolation runs of the scratch PR, a quarter to a third of the OEIS fixture. test_gold_proofs runs every one of those proofs through Comparator against our spec, and Comparator compares the whole statement closure before accepting, so the oracle was a weaker form of a check that already runs.
The compile gate's xargs default of 4 left the 64-core runner idle: 607 s for the 492 OEIS specs against 199 s at 16 jobs in the scratch PR, and 107 s against 38 s for fc100. The tests now pass APN_COMPILE_JOBS = min(cpu count, 16) into the sandbox exec; 16 stayed well inside the generate container's 32 GiB limit in that run. The script's own default is unchanged for the vendor-time dev container.
Every pytest job's log now ends with pytest's setup/call/teardown table for its slowest phases, so the next CI-time question can be answered from the logs of the run at hand instead of a data-collection PR.
tadamcz
force-pushed
the
ci-restructure
branch
from
September 24, 2026 14:36
b91a85e to
d6c81db
Compare
…t comparison" This reverts commit e9a2c33.
The two single-file acceptance cases stay in the suite as well as in test_pin_smoke.py; at the OEIS pin they run twice.
A fixture called pin that yields one hardcoded value reads as parametrized when it is not. The three comparator suites now define PIN = fc_commit(OEIS_DIR) and IMP at module level and use them directly; conftest keeps only the parametrized every_pin.
…ated from Python The pin-smoke job built four pins' images back to back, 36 minutes in the last run. A pins job now prints apn.dataset.FC_PINS as JSON and pin-smoke fans out over it with fromJSON, one job per pin, so the pin list still lives only in Python. Each job runs the two per-pin modules with a new --fc-pin option (conftest), which rejects an unregistered pin. all-checks needs both new jobs, so a failure in the generator fails the run rather than skipping the pins.
…rop the smoke module Instead of a hand-picked smoke module, the per-pin job runs three whole files at each registered pin: test_proof_acceptance.py (back to main's version, with the pin/imp fixtures; pin is now the parametrized fixture, filtered by --fc-pin), test_agent_image.py (Loogle's binary and index are the one agent chunk built per pin) and test_comparator_primitives.py. The standalone agent-image job is the OEIS pin's instance of that and goes. Per pin this is about 2.5 min of acceptance checks and 2 min of agent contract on top of the image build, in parallel jobs, so time-to-green is unchanged.
tadamcz
changed the title
…pin suite now The comparator-tests entry still listed test_proof_acceptance.py after it became pin-parametrized, so that job built all four pins' images and ran the suite at each, 42 minutes instead of about 22. It now runs only the two battery suites.
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.
Follow-up to the timing run in #68, which put time-to-green at 85 to 116 minutes: every job rebuilt its Lean images from an empty cache, the comparator battery ran at all four pins in one serial job, and the five isolation suites ran back to back. This PR restructures which tests run where; it does not touch how images are built.
What runs where now
test_lean_vuln_e2e.pyandtest_comparator_security.pyrun once, at the OEIS pin, via module constantsPINandIMP. Comparator's verdict logic and the checker's staging do not vary with the pin.test_proof_acceptance.py,test_agent_image.pyandtest_comparator_primitives.pyrun at each pin inapn.dataset.FC_PINS: the image builds, an honest proof and disproof are accepted, Lake resolves helper modules, Loogle's per-pin binary and index work, and the comparator primitives resolve.pinis the parametrized fixture;--fc-pinrestricts it to one pin and rejects an unregistered one.pinsjob printsFC_PINSas JSON andper-pinfans out over it withfromJSON, so no pin is listed in the workflow.all-checksneeds every other job and fails unless all succeeded; branch protection should require that one status.testsjob selects by--ignoreonly, so a module listed in no job runs there. Apinsfailure skipsper-pin, whichall-checksreports as failure.--durations=25on every pytest job, so the next timing question is answered from the log at hand.History also contains a removal of the OEIS isolation oracle and its revert; the oracle stays.
Measured
Run 36015119047 on this branch, before the per-pin fan-out, against #68 on the same runner class:
That run's VM was 25 to 30 percent slower than #68's on the unchanged jobs, so the improvement is understated. The serial per-pin job in that run took 36 min; the fan-out replaces it with four parallel jobs of roughly 12 min each.
Not in this PR
Sharding the gold sweep, which is now the critical path; any image-build cache; trimming duplicate cases in the battery.