perf: make /check-golf --measure take minutes instead of hours#1400
Merged
jstoobysmith merged 3 commits intoJul 10, 2026
Conversation
The measure-path file selection in scripts/check_golf.py references a nonexistent FileReport attribute (def_body_changed); the field is named def_value_changed. Every /check-golf --measure run since leanprover-community#1356 crashes with an AttributeError after building the head, so the report comment is never updated. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
…arallel measure) Three changes that turn a ~2h run into minutes: 1. Cache .lake/build across check-golf runs (keyed on toolchain+manifest, restore-keys pick the most recent entry), so the head build is incremental instead of from-scratch (~40 min saved). 2. Build only the changed modules' dependency cones instead of the whole library: measurement only needs the measured files' imports built. 3. Measure files concurrently (--measure-jobs, default nproc). Heartbeats are deterministic and unaffected by parallelism; wall-clock times are measured under load, so only large time deltas remain meaningful (documented in the docstring). Also run scripts/check_golf.py from the default branch rather than the PR head, so the workflow file and script can never skew apart (the failure mode that broke /check-golf on PRs predating leanprover-community#1356). Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
Contributor
|
Thank you for this PR, which will now be reviewed. If submitting to ./Physlib or ./QuantumInfo, please see our review guidelines if you are not familiar with the process. You should expect a back and forth with a reviewer before your PR is merged. See also that link for how to add appropriate labels to your PR. The PR will also go through a number of automated checks. You can learn more about these here, including how to run them locally. If you are submitting to ./PhyslibAlpha there will be a lighter review process, though your PR must still pass the automated checks. If you want to bring attention to this PR, please write a message on this thread of the Lean Zulip. Important: If a reviewer adds an |
jstoobysmith
reviewed
Jul 9, 2026
Member
|
awaiting-author |
github-actions
Bot
added
the
awaiting-author
jstoobysmith
added
ready-to-merge
Vilin97
added a commit
to Vilin97/physlib
that referenced
this pull request
Jul 10, 2026
- CKMMatrix/Basic: the nine phase-shift component lemmas now use squeezed simp only [...] sets instead of broad simp (review: 'a bit bad as not simp only'). - Grad: replace the rw-with-hypothesis ending of distGrad_eq_sum_basis by a direct (distGrad_inner_eq ..).trans h1.symm term (review: 'odd'). - Remove scripts/__pycache__/check_golf.cpython-312.pyc that entered via the leanprover-community#1400 merge. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
jstoobysmith
pushed a commit
that referenced
this pull request
Jul 11, 2026
Running scripts/check_golf.py locally leaves __pycache__/ behind, and one .pyc already slipped into a commit once (#1400, since removed). Ignore Python bytecode so it cannot happen again. Co-authored-by: Claude Fable 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
2 participants
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.
A
/check-golfrun on a large golf PR (e.g. #1364, 129 changed files) currently takes ~2 hours: ~40 min building the head from scratch, then ~90 min measuring files strictly sequentially. Three changes bring this to minutes:.lake/buildacross runs (actions/cache, keyed on toolchain+manifest with restore-keys picking the most recent entry) — the head build becomes incremental instead of from-scratch.--measure-jobs, defaultnproc). Heartbeats — the headline metric — are deterministic and unaffected by concurrency; wall-clock times are measured under load, so only large time deltas remain meaningful (noted in the docstring).Also runs
scripts/check_golf.pyfrom the default branch instead of the PR head, eliminating the workflow/script version-skew failure that broke/check-golfon PRs predating #1356.Expected: ~5–8 min on the standard 4-core runner for a 129-file PR with a warm cache (first run seeds the cache), and ~2–4 min for typical golf PRs.
Stacked on #1399 (includes its one-line fix).
🤖 Generated with Claude Code