Repository navigation
Make /review and /profile refactor-aware - #262
Merged
Merged
Conversation
Detect whether a PR adds a new project or refactors projects already in the
pool — the same added-vs-modified split /profile uses — and handle each
appropriately.
/review (python/lean_pool/review.py): classify_pr() reads PR file statuses
and routes new-project PRs to the existing fit/significance rules
(.github/REVIEW_RULES.md) and refactor PRs to new tech-debt rules
(.github/REFACTOR_REVIEW_RULES.md) — brittle automation, lost structure,
perf regressions, reusability lost. The comment header, assessment table,
and rules link switch by kind.
/profile statement stat (scripts/proof-profile/statements.py): a stdlib-only
port of physlib's check_golf.py declaration parser, trimmed to statement
comparison, reporting how many declarations — and which — changed their
statement rather than only their proof/body. render.py surfaces it for
modified files ("N statements changed" / "no statements changed"); the
report job fetches the new module. Two fixes over the check_golf original:
a line-leading absolute-value bar in a type is no longer misread as an
equation-compiler arm, and _-prefixed unused-hypothesis renames are reported
separately (proposition unchanged) rather than as statement changes.
Tested on the two large golfs on main, #246 (simp_all sweep) and #187
(whole-library compression): both show 0 real statement changes.
Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01QDRfjJLhVEoZ9WQaYwGUgC
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
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.
Makes
/reviewand/profiledetect whether a PR adds a new project or refactors projects already in the pool — the same added-vs-modified split/profilealready uses — and handle each appropriately./review— refactor vs. new-projectclassify_pr()(python/lean_pool/review.py) reads PR file statuses via the GitHub API. A project directory that appears only through added.leanfiles is a new project → the existing fit/significance review (.github/REVIEW_RULES.md, unchanged). A PR that only changes projects already in the pool is a refactor → a new tech-debt review (.github/REFACTOR_REVIEW_RULES.md): brittle automation (structured proof → opaquesimp_allthat breaks on Mathlib bumps), lost proof structure, compile-cost regressions, reusability lost. The comment header, assessment table (scope / tech-debt / maintainability / brittleness / risk), and rules-link switch by kind. No workflow change needed — classification runs insidereview.py./profile— statement-change statNew⚠️ K changed" with the list — the reassurance that a refactor restated no theorem. It runs on pure text (no build), so it shows even when the heartbeat comparison is skipped, and is absent for new-project PRs. The report job fetches the new module.
scripts/proof-profile/statements.py: a stdlib-only port of physlib'scheck_golf.pydeclaration parser, trimmed to statement comparison. It ignores proof golf, definition-body edits, andby-blocks embedded in a type, flagging only genuine type changes.render.pyreports, for modified files, "✅ No statements changed — all N tracked declarations kept their type" or "Two fixes over the
check_golforiginal (both also affect the live parser upstream):|x| ≤ ε, common in analysis/number theory) is no longer misread as an equation-compiler arm — an arm's=>must precede any top-level:=/where._-prefixed unused-hypothesis renames (hM→_hM) are alpha-equivalent, so they're reported in a separatebinder_renamedbucket (proposition unchanged) rather than as statement changes.Validation
Ran both on the two large golfs on
main:tryAtEachStep simp_all#246 (tryAtEachStep simp_all, 1137 files): 0 statement changes; refactor review →needs_discussion(baresimp_allis brittle to simp-set drift).approve(targetedsimpa only/rwakeep their lemma lists; dead-code removal improves maintainability).156 pytest pass (new: classification + refactor rendering in
test_review.py, parser intest_statements.py); ruff clean. Infra/tooling/docs only — noLeanPool/content.🤖 Generated with Claude Code
https://claude.ai/code/session_01QDRfjJLhVEoZ9WQaYwGUgC