Run the correctness oracle nightly in CI, and split what 'pass' means - #4234
Merged
Merged
Conversation
The oracle had only ever run on a laptop. There it silently used a t27c built eight days earlier from uncommitted source and reported 541 passing specs; the same corpus measured with a t27c built from master was 279. Local measurement is also exactly what the operator ruled out for recurring swarm work: anything that should happen on a schedule runs in the cloud. This job builds t27c from the commit it judges and prints that commit beside every count, installs the zig the oracle's numbers were taken with, runs tools/oracle/run.sh, and writes the result to the job summary. Nightly rather than per pull request: a t27c build plus a zig run over ~950 specs is tens of minutes, and the per-PR queue was measured saturated today. The summary splits PASS in two, because `zig test` exits 0 for a file with no test in it. Measured on master today: 553 specs compile, but 347 of them carry no test, so only 206 are verified by one. Reporting 553 as "passing" would repeat an overstatement already made once. The run step is continue-on-error for now. tools/oracle/baseline.tsv still records `pass 541` from the stale compiler, and the ratchet inside run.sh would fail against a number that never existed. The baseline is regenerated from this job's output before the ratchet is allowed to gate. Report step verified locally against a real results.tsv; it reproduces 553 / 206 / 347 / 10 / 382 exactly. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
tools/oracle/run.sh now bounds each spec and emits TIMEOUT for a test that never returns (#4235). Without a row for it the summary would silently drop those specs from every column. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
This was referenced Sep 17, 2026
tools/oracle/run.sh now records a failed t27c gen as NOGEN instead of testing the fragment it left behind (#4235). Without a row the summary drops them, and the table no longer adds up to the corpus. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
This was referenced Sep 17, 2026
Open
This was referenced Sep 17, 2026
Merged
Contributor
|
📓 NotebookLM Notebook linked to this PR
This notebook contains session context, decisions, and artifacts for this work. |
Contributor
Contributor
PR DashboardGenerated at: 2026-09-17 12:26:43 UTC
Summary
Seal Status
|
Contributor
|
📓 NotebookLM Notebook linked to this PR
This notebook contains session context, decisions, and artifacts for this work. |
Contributor
PR DashboardGenerated at: 2026-09-17 12:29:46 UTC
Summary
Seal Status
|
Contributor
|
📓 NotebookLM Notebook linked to this PR
This notebook contains session context, decisions, and artifacts for this work. |
gHashTag
added a commit
that referenced
this pull request
Sep 19, 2026
`check_pr_branch_filters.py` keeps a ceiling on workflows in neither of its lists, and it moves down only. The population had crept back to 27 because `oracle-nightly.yml` landed in #4234 unclassified - exactly the slack the ceiling refuses - and this branch's `spec-parse-ratchet.yml` made 28. Three are classified here: the parse ratchet and `l1-traceability.yml` as merge-critical (a branch filter would hide either on a stacked pull request), `oracle-nightly.yml` as not (it measures the corpus nightly, it does not gate a merge). Population 25, ceiling follows to 25. Refs #4276 Gates: python3 scripts/ci/check_pr_branch_filters.py -> exit 0, 23 + 5 + 25 = 53; --self-test -> exit 0 ("one new unclassified workflow fails"). Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
gHashTag
added a commit
that referenced
this pull request
Sep 19, 2026
* ci: a spec that parsed must not stop parsing `t27c spec-status` over the corpus: 68 NOPARSE on 2026-09-14, 68 on 09-16, 90 on 09-17. A spec that does not parse generates nothing, so the tests it carries stop running; #4272 repaired fourteen of them only by taking back the version the bee had written. Nothing caught them. The required checks are validate and check-linked-issue, and neither runs the compiler over a changed spec. This gate asks one question over the files a change touches: did a spec that parsed at the base stop parsing? Already-broken specs are not its business and a new file cannot regress. A compiler that cannot be run exits 2 - could not run, not a pass. Closes #4276 Gates: python3 tools/ci/check_specs_still_parse.py --self-test -> ok (7 shapes); against the real t27c, a branch that breaks specs/tri/sort/tim_sort.t27 exits 1 naming the parse error, an unrelated change exits 0, a missing compiler exits 2; python3 scripts/ci/check_pr_branch_filters.py exits 0. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> * ci: classify the new gate, and the nightly I landed without classifying `check_pr_branch_filters.py` keeps a ceiling on workflows in neither of its lists, and it moves down only. The population had crept back to 27 because `oracle-nightly.yml` landed in #4234 unclassified - exactly the slack the ceiling refuses - and this branch's `spec-parse-ratchet.yml` made 28. Three are classified here: the parse ratchet and `l1-traceability.yml` as merge-critical (a branch filter would hide either on a stacked pull request), `oracle-nightly.yml` as not (it measures the corpus nightly, it does not gate a merge). Population 25, ceiling follows to 25. Refs #4276 Gates: python3 scripts/ci/check_pr_branch_filters.py -> exit 0, 23 + 5 + 25 = 53; --self-test -> exit 0 ("one new unclassified workflow fails"). Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> --------- Co-authored-by: Claude Opus 5 <noreply@anthropic.com>
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.
Refs #3903
The correctness oracle has only ever run on a laptop — and on the laptop it was wrong. It silently used a
t27cbuilt eight days earlier from uncommitted source and reported 541 passing specs. The same corpus, measured with at27cbuilt from master, was 279.That is also what the operator ruled out for the swarm: recurring work runs in the cloud, not on a machine that sleeps.
What it does
Once a day on master: builds
t27cfrom the commit it judges (and prints that commit beside every number), installs the zig the oracle's measurements were taken with, runstools/oracle/run.sh, and writes this to the job summary:plus the largest failure classes, and the full
results.tsvas an artifact.Those are master
5719414eemeasured with the NOGEN and TIMEOUT fixes from #4235. The first version of this description showed 553 / 206 / 347 — inflated: that run kept a failed generation's fragment and let it pass. The Report step reproduces the corrected table exactly.Why PASS is split
zig testexits 0 for a file with no test in it. 39 of the 189 compiling specs on master carry no test (257 of 462 once #4114 lands), so for them "pass" means only "compiles". Only 206 are verified by a test. A single PASS column would overstate it — and that overstatement was already made once, in #4114, and corrected there.Why nightly, not per PR
A
t27cbuild plus zig over ~950 specs is tens of minutes, and the per-PR queue was measured saturated today (60 runs queued, not draining). Nightly catches a regression the day it lands without adding to that.Why the run step is not fatal yet
tools/oracle/baseline.tsvstill sayspass 541, from the stale compiler. The ratchet insiderun.shwould fail against a number that never existed. This job's output is what the baseline gets regenerated from; after that, the ratchet can gate.Read-only:
permissions: contents: read, no secrets, nothing pushed.🤖 Generated with Claude Code