Conversation
Workflow runs on the self-hosted runner: a test job (release build, cargo test with default and arena_compact+random features, docs) and a bench job that benchmarks the PR head against its base on the same machine. bench_ab.sh builds both sides once, runs them in alternating order pinned to one core, averages the rounds with bench_avg_files.py and posts the bench_cmp.py table to the step summary and the PR. Co-Authored-By: Claude Fable 5.1 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01QXEKcXZn55RYJY7BSJuYeS
…ning bench_ab.sh failed on the runner with exit 101 because act_paths declares required-features (arena_compact, serialization) and the script built without them. It now reads each side's Cargo.toml and passes the features the requested benches need, and prints the cargo error into the step log when a build fails instead of leaving it in a temp file. The script also appends to progress.txt after every run and rewrites compare.txt after every completed round. The workflow runs it in the background and, once a minute, posts progress plus the compare table of the rounds finished so far to one PR comment via pr_comment.py (stdlib only). The comment is found by a marker so re-runs and later pushes reuse it, and its id is cached per run so the periodic updates skip the lookup. This replaces the sticky-comment action. Co-Authored-By: Claude Fable 5.1 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01QXEKcXZn55RYJY7BSJuYeS
…th results The per-minute progress updates duplicated the job log. The comment now carries a link to the specific job (looked up from the run's jobs as the one in progress on this runner, falling back to the run link) and, when the bench finishes, the compare table. Co-Authored-By: Claude Fable 5.1 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01QXEKcXZn55RYJY7BSJuYeS
… run The table for a bench is averaged over the rounds finished so far and saved as cmp-<bench>.txt; compare.txt is the concatenation, rewritten at the end of every round. Co-Authored-By: Claude Fable 5.1 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01QXEKcXZn55RYJY7BSJuYeS
Co-Authored-By: Claude Fable 5.1 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01QXEKcXZn55RYJY7BSJuYeS
The crate on master has 44 new divergences from the Lean model on the seed-7 corpus, so "zero divergences" cannot be the bar. fuzz_ab.sh runs head and base on identical inputs (model vs crate, 20000; ACT read side, 5000) and fails only when head diverges on an input base did not. Both sides use head's differential/ and lean/, so only the crate under test differs; if base cannot be built with head's harness its own is tried, and with no baseline at all the job reports that and does not gate. Two enabling fixes: the differential harness did not compile since the ZipperValues/ZipperValuesAt split (ReadSource now requires ZipperValuesAt<u64>), and differential.py accepts PATHMAP_TRACE / PATHMAP_ACT_TRACE to find binaries built into another target dir. The fuzz job runs after the tests, on PRs and manual runs. Lean is installed through elan for the runner user; lake's build dir is kept in the runner's cache since checkout wipes ignored files. Co-Authored-By: Claude Fable 5.1 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01QXEKcXZn55RYJY7BSJuYeS
Same inputs, env vars and output files as the bash versions, which were mostly embedded Python anyway. bench_ab.py imports the divan helpers from benches/ instead of shelling out to bench_avg_files.py and bench_cmp.py. Standard library only. Co-Authored-By: Claude Fable 5.1 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01QXEKcXZn55RYJY7BSJuYeS
Co-Authored-By: Claude Fable 5.1 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01QXEKcXZn55RYJY7BSJuYeS
bench_ab.py now also writes summary.md and summary.json after every round: one row per bench (cases, geometric mean, largest gain and loss, counts beyond 5%) and a collapsed list of the cases that moved more than 5%. The PR comment and the run summary use it; the full per-bench tables stay in the job log and the bench-out artifact. Co-Authored-By: Claude Fable 5.1 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01QXEKcXZn55RYJY7BSJuYeS
Co-Authored-By: Claude Fable 5.1 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01QXEKcXZn55RYJY7BSJuYeS
Co-Authored-By: Claude Fable 5.1 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01QXEKcXZn55RYJY7BSJuYeS
The job stays green; the run shows the annotation and the summary names the inputs. FUZZ_STRICT=1 restores the hard failure (with an error annotation). A run that does not finish still fails the job. Co-Authored-By: Claude Fable 5.1 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01QXEKcXZn55RYJY7BSJuYeS
For up to FUZZ_REPROS (3) newly diverging inputs with distinct first-differing operations, fuzz_ab.py runs lean/shrink.py on the saved input and `pathmap_trace --repro` on the result. The summary gets a collapsed block per input with the differing trace lines and the Rust program; the .min.bin and .rs files go to fuzz-out/repro/ in the artifact. shrink.py accepts PATHMAP_ORACLE / PATHMAP_TRACE / PATHMAP_ACT_TRACE like differential.py. Co-Authored-By: Claude Fable 5.1 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01QXEKcXZn55RYJY7BSJuYeS
Co-Authored-By: Claude Fable 5.1 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01QXEKcXZn55RYJY7BSJuYeS
The toolchain step resolves lean/lean-toolchain through elan (which downloads it when missing) and prints the versions; fuzz_ab.py reports each lake and cargo build with its duration instead of only on failure. Co-Authored-By: Claude Fable 5.1 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01QXEKcXZn55RYJY7BSJuYeS
A clean runner has neither. Every job's toolchain step now installs rustup into $HOME if absent and puts it on the PATH; the fuzz job does the same for elan and resolves lean/lean-toolchain there, which fetches the pinned Lean. Verified from an empty home with a bare PATH: rustup, stable Rust, elan and Lean 4.33.1 all arrive in about 20 seconds. Co-Authored-By: Claude Fable 5.1 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01QXEKcXZn55RYJY7BSJuYeS
Each bench's base and head runs still share one core back to back, but different benches run at the same time on different cores from BENCH_CPUS (default: one SMT thread per physical core, every other core, at most 16, which spreads them over the L3 complexes). A round's wall time is now that of its slowest bench pair rather than the sum. Co-Authored-By: Claude Fable 5.1 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01QXEKcXZn55RYJY7BSJuYeS
An A/A run (same commit on both sides) reported 5-25% differences on superdense_keys and binary_keys cases, consistent across rounds, with the two sides pinned to the same core. The sides were different binaries: built at different paths into different target dirs, they got different crate hashes and code layout. Now one worktree is used for both: check out base, build, copy the bench executables out; check out head, build, copy out. The historical bench run did the same and had a round-to-round CV under 1% on those benches. Co-Authored-By: Claude Fable 5.1 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01QXEKcXZn55RYJY7BSJuYeS
`lake build` type-checks the theorems in Spec.lean and evaluates every #guard in Check.lean, so a broken law or regression fixture fails the job. Lean only warns on sorry, so the job greps the build log and the model sources for it (and for axioms) separately. Lake's build dir is kept in the runner's cache; a warm run takes seconds. Co-Authored-By: Claude Fable 5.1 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01QXEKcXZn55RYJY7BSJuYeS
pr_comment.py takes --id / --title / --dir so each job owns one comment per PR (bench keeps its marker and defaults). The fuzz job posts its summary after every run: verdict, per-mode tables, the inputs that diverge on head but not on base, and the shrunk Rust reproducers in collapsed blocks. Co-Authored-By: Claude Fable 5.1 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01QXEKcXZn55RYJY7BSJuYeS
Its findings are warnings, and a PR with failing tests is one whose divergences are worth seeing. The bench job still needs both to pass. Co-Authored-By: Claude Fable 5.1 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01QXEKcXZn55RYJY7BSJuYeS
One row per first-differing operation (or final-state mismatch) with the input count and a first example, instead of up to 50 inputs. Co-Authored-By: Claude Fable 5.1 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01QXEKcXZn55RYJY7BSJuYeS
fuzz_ab.py writes a findings file when head has new divergences or a run did not finish; pr_comment.py --create-only-if creates the comment only then. An existing comment is still updated by a clean run, so it does not keep showing stale findings. Co-Authored-By: Claude Fable 5.1 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01QXEKcXZn55RYJY7BSJuYeS
The comparison diffs only the unclassified divergences, so inputs that moved between the known-bug bucket and agreement were invisible: a base with 826 known hits and a head with 221 showed 44 new on both sides and nothing fixed. The summary now has a legend and a table of known classes whose hit counts differ between base and head. Co-Authored-By: Claude Fable 5.1 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01QXEKcXZn55RYJY7BSJuYeS
imlvts
force-pushed
the
ci-self-hosted
branch
from
September 15, 2026 22:50
0db035c to
09d5aa5
Compare
differential.py derived the agreement count by subtracting from the requested input count, so when --max-fails stopped the run early every input that was never executed was scored as agreeing. The error grows with the number of divergences, which is backwards: over 3000 inputs at seed 7, --max-fails 3 classified 846 inputs and reported 2987/3000 agree -- more than the 2959/3000 an exhaustive run finds over the same set. --max-fails defaults to 10, so hand-run invocations were all affected; fuzz_ab.py passes --max-fails 0 and was exact. Count the inputs actually classified and report against that, naming the shortfall on a line of its own so the summary line's format, which fuzz_ab.py parses with SUMMARY_RE, is unchanged. A denominator below the requested count now counts as an unfinished run in fuzz_ab.py, which fails the job. A truncated run previously still printed a summary line and passed as OK, even though the two sides stop after their own scheduling-dependent prefix of the inputs: comparing failure sets drawn from different input populations is not a gate. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
Every skip rendered as a bare `skip`, so a trace said that something declined the operation but not what: the ACT read source refusing to be a merge source, a degenerate `k = 0`, an empty focus and a quarantined op were all the same token. Each site now emits `skip:<reason>` from a vocabulary defined once on each side -- `SKIP_*` in harness.rs, `skip*` in Fuzz.lean -- and the two must agree exactly, since a token that differs makes every input that skips diverge. Naming them turned up an ordering bug the bare token had hidden. For `restricting` the model tested ACT mode first and the harness tested the empty focus first, so in ACT mode with an empty focus the two took different branches and agreed only because both printed `skip`. The model now checks the guards in the harness's order; the harness reaches its ACT skip only by calling `do_restricting`, which it does not do once the empty-focus guard has fired, so that is the order that can be matched. `meet_k_path_into` splits `meetKPathUnspecified` into its two disjuncts on both sides for the same reason. Behaviour is otherwise unchanged: 20000 crate inputs and 5000 ACT inputs at seed 7 give the same agree, known and new counts as before. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
At seed 7 the run reported 44 unclassified divergences on 20000 crate inputs and 3 on 5000 ACT inputs. All of them are instances of five defects the 2026-09-11 triage had already shrunk into lean/corpus/ but that were never added to KNOWN, so every run rediscovered them and a genuinely new defect would have had to be spotted among them. They resisted the existing op-name keys because the op that reports one is not the op that caused it: value bias is introduced by a merge but observed by whichever of `dump`, `val_at` or the final map dump next reads the location, and it turned up under six different op names. So `divergence_shape` keys them on which fields of the trace line moved -- status only, a child count that grew, a value count that shrank, a value that changed, the focus value returned for a path the model says is empty -- and the KNOWN entries match those tags. They are tested last, so every op-specific entry above still wins. Returning "no familiar shape" is the case that matters, and the shapes are deliberately narrow: a value appearing or vanishing is not value bias, a location moving in a dump is not, and a bool return flipping is not, which is why the value-bias rule for `ret` is confined to the ops whose return is a value rather than a flag. A compound divergence on seed 10 (`meet_k_path_into` flips its bool, drops a value and gains a child at once) is still reported as new, which is correct. Also fixes a misattribution: the ACT val_count shape entry sat below the op-name entries, so a val_count-only difference landing on a `to_next_val` line was blamed on the `to_next_val` class -- 131 of 5000 ACT inputs at seed 7. It is tested first now. Seed 7 goes from 44 and 3 new to 0 and 0 with the agree counts unchanged, seeds 0-3, 11 and 99 from 1-2 new to 0, and all 14 corpus reproducers classify as the class their filenames name. Co-Authored-By: Claude Opus 5 (1M context) <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.
Here's how it looks like:
Fuzzing result: imlvts#2 (comment)
Benches result: imlvts#1 (comment)