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
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)