From 10d99713c798a02a459210db190c2b2846a10263 Mon Sep 17 00:00:00 2001 From: Vasily Ilin Date: Sun, 19 Jul 2026 23:38:16 -0700 Subject: [PATCH] Make /review and /profile refactor-aware MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit 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 Claude-Session: https://claude.ai/code/session_01QDRfjJLhVEoZ9WQaYwGUgC --- .github/REFACTOR_REVIEW_RULES.md | 110 +++++ .github/instructions/review.instructions.md | 10 +- .github/workflows/proof-profile.yml | 14 + python/lean_pool/review.py | 216 +++++++++- python/tests/test_review.py | 81 ++++ python/tests/test_statements.py | 130 ++++++ scripts/proof-profile/render.py | 155 ++++++- scripts/proof-profile/statements.py | 451 ++++++++++++++++++++ 8 files changed, 1144 insertions(+), 23 deletions(-) create mode 100644 .github/REFACTOR_REVIEW_RULES.md create mode 100644 python/tests/test_statements.py create mode 100644 scripts/proof-profile/statements.py diff --git a/.github/REFACTOR_REVIEW_RULES.md b/.github/REFACTOR_REVIEW_RULES.md new file mode 100644 index 0000000000..490897a274 --- /dev/null +++ b/.github/REFACTOR_REVIEW_RULES.md @@ -0,0 +1,110 @@ +# Refactor Review Rules + +You are a senior Lean engineer reviewing a **refactor** pull request to +**Lean Pool**. A refactor PR modifies files in projects that are *already in +the pool* — proof golf, `simp`/`grind`/`aesop` rewrites, module +reorganizations, API renames, extracting or inlining lemmas. It does **not** +add a new project. + +Because the project is already accepted, the merge decision is *not* about +mathematical fit or significance — those were settled when the project landed. +The maintainer's question here is narrower: **does this refactor leave the +code in a better or worse state to maintain?** Your job is to answer that — +first as a one-paragraph narrative, then as a short structured assessment, +then with a verdict. Write to a colleague: direct, no encouragement, no +"nice cleanup." + +## What to look for + +The central risk in a refactor — especially an automated golf — is **trading +readability and robustness for line count**. Flag it where you see it: + +- **Brittle automation.** A structured, multi-step proof collapsed into a + single opaque `simp_all` / `aesop` / `grind` / `omega` / `decide` is shorter + but more fragile: it can silently break on the next Mathlib bump (simp-set + drift, lemma renames, changed defaults) and gives no foothold for debugging + when it does. The heavier and less targeted the tactic, the higher the debt. + A `simp only [...]` with an explicit lemma list is far more robust than a + bare `simp_all`. (This is the one place where `simp` vs `simp only` *is* in + scope — for a refactor it is a maintainability signal, not a style nit.) +- **Lost structure.** Golf that deletes the intermediate `have`s, named + witnesses, or case labels that documented the mathematical argument, leaving + a proof that compiles but no longer *reads*. +- **Compile-cost regressions.** A rewrite that makes a proof materially slower + or hungrier (the `/profile` heartbeat/wall table is the evidence — cite it + when a golfed proof got more expensive). +- **Reusability lost.** A helper lemma that had multiple callers inlined away, + or a generalization narrowed, so future work has to redo it. +- **Dead or confused leftovers.** Half-applied renames, orphaned lemmas that + now have no caller, comments that no longer match the code. +- **Anything else** that a maintainer would regret six months later. + +A refactor that is *only* mechanical (whitespace, joining tactic lines, +reflowing) or that genuinely improves clarity/robustness is a clean `approve` +with an empty `findings` list — say so plainly. + +## Out of scope — do not flag + +Caught by linters and other CI elsewhere; or already reported by other tools: + +- Presence of `sorry`, `admit`, or new `axiom` declarations. +- Whether the refactor changed any *statement* — the `/profile` comment + already reports exactly which declarations changed their statement. Do not + re-derive that; assume statements are preserved unless the diff makes an + obvious signature change you should mention. +- File headers, copyright, license, authorship, naming conventions + (`camelCase` vs `snake_case`), line length, trailing whitespace, ASCII. +- File-size or proof-size limits; `set_option maxHeartbeats` overrides. +- `decide` / `native_decide` justification comments. +- Presence of docstrings on public declarations. +- `import` redundancy in the auto-generated root `LeanPool.lean`. + +## Output + +Return a single JSON object: + +```json +{ + "summary": "", + "assessment": { + "scope": "", + "introduces_tech_debt": , + "maintainability": "improved" | "unchanged" | "regressed", + "brittleness": "more_robust" | "unchanged" | "more_brittle", + "risk": "low" | "medium" | "high", + "assessment_one_sentence": "" + }, + "verdict": "approve" | "request_changes" | "needs_discussion", + "findings": [ + { + "file": "", + "line": , + "rule": "", + "comment": "" + } + ] +} +``` + +The `assessment` block is the core deliverable. `findings` is for specific, +actionable concerns — an empty list is fine and often correct for a clean +mechanical golf. + +Verdict mapping: + +- `approve` — the refactor is net-neutral or an improvement; no tech debt a + maintainer needs to act on before merging. +- `request_changes` — it introduces tech debt or brittleness serious enough + that the maintainer should fix it (or ask the author to) before merging. +- `needs_discussion` — a genuine trade-off the maintainer should weigh (e.g. + a large `simp_all` golf that is shorter and passes today but measurably more + fragile), where reasonable people could go either way. + +## Style + +- One paragraph summary. Prose, not a bullet list of every changed file. +- Be direct. No editorializing, no encouragement. +- When in doubt about a finding, omit it. Less noise → higher trust. +- On a pool-wide golf touching hundreds of files, do not enumerate files. + Characterize the *pattern* and point at the two or three most telling + examples. diff --git a/.github/instructions/review.instructions.md b/.github/instructions/review.instructions.md index ec6e3aa167..2717c8b5de 100644 --- a/.github/instructions/review.instructions.md +++ b/.github/instructions/review.instructions.md @@ -4,9 +4,13 @@ applyTo: "**" # Lean Pool — review instructions -When reviewing a pull request to this repository, follow the rules in -[`.github/REVIEW_RULES.md`](../REVIEW_RULES.md). Summary below for -convenience; the rules doc is authoritative. +Reviews split by PR kind, the same way `/profile` does. A PR that adds a +**new project** is reviewed for fit and significance — follow +[`.github/REVIEW_RULES.md`](../REVIEW_RULES.md) (summarized below). A +**refactor** PR (proof golf, tactic rewrites, reorganizations of projects +already in the pool) is reviewed for tech debt and maintainability instead — +follow [`.github/REFACTOR_REVIEW_RULES.md`](../REFACTOR_REVIEW_RULES.md). The +rules docs are authoritative; the summary below covers the new-project case. ## Your job diff --git a/.github/workflows/proof-profile.yml b/.github/workflows/proof-profile.yml index 84312c9b14..d02eadef31 100644 --- a/.github/workflows/proof-profile.yml +++ b/.github/workflows/proof-profile.yml @@ -15,6 +15,13 @@ name: Proof Profile # cache exists) the comparison is skipped and modified files fall back to # the absolute profile. # +# Modified files also get a textual statement-change report (statements.py, +# the same parser physlib's /check-golf uses): how many declarations — and +# which — changed their *statement* rather than only their proof/body. This +# needs no build, so it renders even when the compile-cost comparison is +# skipped; it is the reassurance a refactor wants that no theorem was quietly +# restated. +# # Speed (same approach as physlib's /check-golf): measurement only needs the # measured files' *imports* built, never the whole library, so `lake build` # targets just the changed modules. Both sides of a comparison are elaborated @@ -523,6 +530,13 @@ jobs: fi done git show origin/main:scripts/proof-profile/render.py > "$RUNNER_TEMP/render.py" + # render.py imports statements.py as a sibling module (both fetched + # to $RUNNER_TEMP, which is render.py's script dir and so on + # sys.path). Fall back to the checkout while it has not landed on + # the default branch yet. + git show origin/main:scripts/proof-profile/statements.py \ + > "$RUNNER_TEMP/statements.py" \ + || cp scripts/proof-profile/statements.py "$RUNNER_TEMP/statements.py" python3 "$RUNNER_TEMP/render.py" # A `pull_request` run from a fork gets a read-only GITHUB_TOKEN and diff --git a/python/lean_pool/review.py b/python/lean_pool/review.py index 3823594629..082cc2f883 100644 --- a/python/lean_pool/review.py +++ b/python/lean_pool/review.py @@ -1,10 +1,14 @@ """LLM-driven pull request review for Lean Pool. -Reads the rules from ``.github/REVIEW_RULES.md``, fetches the PR diff via the -GitHub CLI, asks the configured OpenAI model to evaluate the contribution, -and posts or updates a sticky PR comment with the reviewed head SHA, a -one-paragraph summary, a structured assessment table (fit / level / branch / -mode / code-quality / etc.), a verdict, and any specific findings. +Detects whether the PR adds a new project or refactors projects already in +the pool — the same added-vs-modified split ``/profile`` uses — and reviews +it under the matching rules. New-project PRs are judged on fit and +significance (``.github/REVIEW_RULES.md``); refactor PRs are judged on tech +debt and maintainability (``.github/REFACTOR_REVIEW_RULES.md``). Either way +it fetches the PR diff via the GitHub CLI, asks the configured OpenAI model +to evaluate the contribution, and posts or updates a sticky PR comment with +the reviewed head SHA, a one-paragraph summary, a structured assessment +table, a verdict, and any specific findings. The reviewer prefers OpenAI's ``flex`` tier (cheaper, slower, occasionally unavailable). When flex returns 429 Resource Unavailable, the request is @@ -44,7 +48,8 @@ from openai import APIStatusError, OpenAI, RateLimitError REPO_ROOT = Path(__file__).resolve().parents[2] -RULES_PATH = REPO_ROOT / ".github" / "REVIEW_RULES.md" +PROJECT_RULES_PATH = REPO_ROOT / ".github" / "REVIEW_RULES.md" +REFACTOR_RULES_PATH = REPO_ROOT / ".github" / "REFACTOR_REVIEW_RULES.md" DEFAULT_MODEL = "gpt-5.5" # Flex tier requests can take longer than the default 10-minute timeout. REQUEST_TIMEOUT_SECONDS = 6000.0 @@ -74,8 +79,22 @@ "borderline": "🟡", "not_a_fit": "🛑", } +# Refactor-assessment icons. Both maintainability and brittleness read +# "green = better after the refactor, red = worse." +DEBT_ICON = {True: "🛑", False: "✅"} +MAINTAINABILITY_ICON = { + "improved": "✅", + "unchanged": "➖", + "regressed": "🛑", +} +BRITTLENESS_ICON = { + "more_robust": "✅", + "unchanged": "➖", + "more_brittle": "🛑", +} +RISK_ICON = {"low": "✅", "medium": "🟡", "high": "🛑"} -SYSTEM_PROMPT = dedent( +SYSTEM_PROMPT_PROJECT = dedent( """\ You are a senior mathematician and Lean engineer reviewing pull requests to Lean Pool, a curated repository of formal-mathematics @@ -97,6 +116,35 @@ """ ) +SYSTEM_PROMPT_REFACTOR = dedent( + """\ + You are a senior Lean engineer reviewing a refactor pull request to + Lean Pool. This PR modifies projects that are ALREADY in the pool — + proof golf, tactic rewrites, module reorganizations, API renames. It + does not add a new project, so mathematical fit and significance are + NOT in question and you must not assess them. + + The maintainer's question is narrower: does this refactor leave the + code better or worse to maintain? Focus on tech debt — proofs made + more brittle (e.g. a structured proof collapsed into an opaque + `simp_all` / `aesop` / `grind` that will break on the next Mathlib + bump and is hard to debug), lost proof structure, compile-cost + regressions, reusability lost, dead leftovers — and on any other + issue a maintainer would regret later. + + Write to a colleague: direct, no encouragement, no "nice cleanup." + For a refactor, `simp` vs `simp only` and heavy-automation brittleness + ARE in scope. Do NOT flag things other CI already covers: sorry / + axioms, headers, naming, line length, maxHeartbeats, or whether any + statement changed (the /profile comment reports that separately). + + Always respond with a single JSON object matching the schema in the + rules document. The `assessment` block is the core deliverable. + `findings` is for specific, actionable concerns; an empty list is + fine and correct for a clean mechanical golf. + """ +) + def run_gh(*args: str, stdin: str | None = None) -> str: """Run ``gh`` with the given arguments and return stdout. @@ -188,8 +236,74 @@ def fetch_head_sha(pr_number: str, repo_full_name: str) -> str: ) -def request_review(model: str, rules: str, diff: str) -> tuple[dict, Any, str]: - """Ask the model to apply ``rules`` to ``diff``. +def fetch_pr_files(pr_number: str, repo_full_name: str) -> list[tuple[str, str]]: + """Return ``(filename, status)`` for every file in ``pr_number``. + + ``status`` is GitHub's file status: ``added``, ``modified``, + ``removed``, ``renamed``, ``changed``, or ``copied``. The endpoint + paginates, so this is safe on PRs that touch thousands of files. + """ + raw = run_gh( + "api", + f"repos/{repo_full_name}/pulls/{pr_number}/files", + "--paginate", + "--jq", + ".[] | [.filename, .status] | @tsv", + ) + files: list[tuple[str, str]] = [] + for line in raw.splitlines(): + if not line.strip(): + continue + name, _, status = line.partition("\t") + files.append((name, status)) + return files + + +def project_of(path: str) -> str | None: + """Return the pooled project a Lean file belongs to, or ``None``. + + Project content lives at ``LeanPool//...``; the auto-generated + root ``LeanPool.lean`` and non-project files return ``None``. + """ + parts = path.split("/") + if len(parts) > 2 and parts[0] == "LeanPool": + return parts[1] + return None + + +def classify_pr(files: list[tuple[str, str]]) -> str: + """Classify a PR as ``"refactor"`` or ``"project"``. + + Mirrors ``/profile``'s added-vs-modified split lifted to the PR level: a + PR that adds a *new project* (a project directory that appears only + through added ``.lean`` files) is a ``"project"`` PR and gets the full + fit/significance review. A PR that only changes files in projects + already in the pool — the pure-golf / reorganization case — is a + ``"refactor"`` and gets the tech-debt review. When no project files are + touched at all, default to ``"project"`` (the conservative review). + """ + added_projects: set[str] = set() + existing_projects: set[str] = set() + for name, status in files: + if not name.endswith(".lean"): + continue + project = project_of(name) + if project is None: + continue + if status == "added": + added_projects.add(project) + else: # modified / removed / renamed / changed / copied + existing_projects.add(project) + new_projects = added_projects - existing_projects + if not new_projects and existing_projects: + return "refactor" + return "project" + + +def request_review( + model: str, rules: str, diff: str, system_prompt: str +) -> tuple[dict, Any, str]: + """Ask the model to apply ``rules`` to ``diff`` under ``system_prompt``. Tries the ``flex`` service tier first; if OpenAI returns 429 Resource Unavailable, retries with ``service_tier="auto"`` (standard tier). @@ -202,7 +316,7 @@ def request_review(model: str, rules: str, diff: str) -> tuple[dict, Any, str]: client = OpenAI(timeout=REQUEST_TIMEOUT_SECONDS) user_content = f"## Review rules\n\n{rules}\n\n## PR diff\n\n```diff\n{diff}\n```" messages = [ - {"role": "system", "content": SYSTEM_PROMPT}, + {"role": "system", "content": system_prompt}, {"role": "user", "content": user_content}, ] @@ -256,8 +370,8 @@ def render_usage(usage: Any, model: str, tier: str) -> str: return " · ".join(parts) -def render_assessment(payload: dict) -> str: - """Render the structured assessment block as a Markdown table.""" +def render_project_assessment(payload: dict) -> str: + """Render a new-project assessment block as a Markdown table.""" a = payload.get("assessment") or {} if not a: return "" @@ -285,19 +399,66 @@ def render_assessment(payload: dict) -> str: return table +def render_refactor_assessment(payload: dict) -> str: + """Render a refactor assessment block as a Markdown table.""" + a = payload.get("assessment") or {} + if not a: + return "" + + debt = a.get("introduces_tech_debt") + debt_cell = ( + f"{DEBT_ICON.get(bool(debt), '•')} {'yes' if debt else 'no'}" + if debt is not None + else "?" + ) + maint = a.get("maintainability", "") + maint_cell = f"{MAINTAINABILITY_ICON.get(maint, '•')} `{maint}`" if maint else "?" + brit = a.get("brittleness", "") + brit_cell = f"{BRITTLENESS_ICON.get(brit, '•')} `{brit}`" if brit else "?" + risk = a.get("risk", "") + risk_cell = f"{RISK_ICON.get(risk, '•')} `{risk}`" if risk else "?" + + rows = [ + ("Scope", a.get("scope", "?")), + ("Introduces tech debt", debt_cell), + ("Maintainability", maint_cell), + ("Brittleness", brit_cell), + ("Risk", risk_cell), + ] + table = "| Aspect | Value |\n|---|---|\n" + for k, v in rows: + table += f"| {k} | {v} |\n" + + sentence = (a.get("assessment_one_sentence") or "").strip() + if sentence: + table += f"\n_{sentence}_" + return table + + def render_comment( payload: dict, model: str, usage: Any, tier: str, reviewed_head_sha: str, + kind: str = "project", ) -> str: - """Render the model's payload as a Markdown PR comment body.""" + """Render the model's payload as a Markdown PR comment body. + + ``kind`` is ``"project"`` (fit/significance review) or ``"refactor"`` + (tech-debt review); it selects the header, the assessment table, and + the rules doc linked in the footer. + """ summary = (payload.get("summary") or "").strip() verdict = (payload.get("verdict") or "").strip() findings = payload.get("findings") or [] - lines = [LLM_REVIEW_MARKER, f"## 🤖 LLM review (`{model}`)", ""] + heading = ( + f"## 🤖 LLM review — refactor (`{model}`)" + if kind == "refactor" + else f"## 🤖 LLM review (`{model}`)" + ) + lines = [LLM_REVIEW_MARKER, heading, ""] if reviewed_head_sha: lines.extend([f"**Reviewed head:** `{reviewed_head_sha}`", ""]) @@ -309,7 +470,11 @@ def render_comment( if summary: lines.extend([summary, ""]) - assessment = render_assessment(payload) + assessment = ( + render_refactor_assessment(payload) + if kind == "refactor" + else render_project_assessment(payload) + ) if assessment: lines.extend([assessment, ""]) @@ -335,9 +500,10 @@ def render_comment( usage_line = render_usage(usage, model, tier) if usage_line: lines.append(usage_line) + rules_doc = "REFACTOR_REVIEW_RULES.md" if kind == "refactor" else "REVIEW_RULES.md" lines.append( "_Automated review against " - "[`.github/REVIEW_RULES.md`](../blob/main/.github/REVIEW_RULES.md). " + f"[`.github/{rules_doc}`](../blob/main/.github/{rules_doc}). " "Disagree? Reply on the PR; rules can be updated in a PR of their own._" ) return "\n".join(lines) @@ -393,7 +559,18 @@ def main() -> int: model = os.environ.get("REVIEW_MODEL", DEFAULT_MODEL) repo_full_name = resolve_repo_full_name().strip() - rules = RULES_PATH.read_text(encoding="utf-8") + + # Detect whether this is a new-project PR or a refactor of projects + # already in the pool, and review it under the matching rules. + kind = classify_pr(fetch_pr_files(pr_number, repo_full_name)) + if kind == "refactor": + rules = REFACTOR_RULES_PATH.read_text(encoding="utf-8") + system_prompt = SYSTEM_PROMPT_REFACTOR + else: + rules = PROJECT_RULES_PATH.read_text(encoding="utf-8") + system_prompt = SYSTEM_PROMPT_PROJECT + print(f"Reviewing PR #{pr_number} as a {kind} PR.", file=sys.stderr) + diff = fetch_diff(pr_number, repo_full_name) if not diff.strip(): @@ -404,13 +581,16 @@ def main() -> int: os.environ.get("REVIEW_HEAD_SHA") or fetch_head_sha(pr_number, repo_full_name).strip() ) - payload, usage, tier = request_review(model=model, rules=rules, diff=diff) + payload, usage, tier = request_review( + model=model, rules=rules, diff=diff, system_prompt=system_prompt + ) comment = render_comment( payload, model=model, usage=usage, tier=tier, reviewed_head_sha=reviewed_head_sha, + kind=kind, ) post_comment(pr_number, comment, repo_full_name=repo_full_name) return 0 diff --git a/python/tests/test_review.py b/python/tests/test_review.py index e2f63d332e..7d3b99037c 100644 --- a/python/tests/test_review.py +++ b/python/tests/test_review.py @@ -40,3 +40,84 @@ def test_render_comment_includes_marker_and_reviewed_head() -> None: assert body.startswith(LLM_REVIEW_MARKER) assert "**Reviewed head:** `abc123`" in body assert "**Verdict:**" in body + # A new-project review links the project rules, not the refactor rules. + assert "REVIEW_RULES.md" in body + assert "REFACTOR_REVIEW_RULES.md" not in body + + +def test_classify_pr_pure_golf_is_refactor() -> None: + """Modifying only existing project files is a refactor.""" + from lean_pool.review import classify_pr + + files = [ + ("LeanPool/Foo/A.lean", "modified"), + ("LeanPool/Bar/B.lean", "modified"), + ("LeanPool.lean", "modified"), + ] + assert classify_pr(files) == "refactor" + + +def test_classify_pr_new_project_is_project() -> None: + """A project that appears only through added files is a new project.""" + from lean_pool.review import classify_pr + + files = [ + ("LeanPool/NewProj/A.lean", "added"), + ("LeanPool/NewProj/B.lean", "added"), + ("LeanPool/projects.yml", "modified"), + ("LeanPool.lean", "modified"), + ] + assert classify_pr(files) == "project" + + +def test_classify_pr_module_split_is_refactor() -> None: + """Adding a file to a project that is also modified stays a refactor.""" + from lean_pool.review import classify_pr + + files = [ + ("LeanPool/Foo/A.lean", "modified"), + ("LeanPool/Foo/ASplit.lean", "added"), + ] + assert classify_pr(files) == "refactor" + + +def test_classify_pr_without_project_files_defaults_to_project() -> None: + """Infra-only diffs fall back to the conservative project review.""" + from lean_pool.review import classify_pr + + assert classify_pr([("README.md", "modified")]) == "project" + + +def test_render_comment_refactor_mode() -> None: + """A refactor review shows the tech-debt table and refactor rules link.""" + from lean_pool.review import LLM_REVIEW_MARKER, render_comment + + body = render_comment( + { + "summary": "Collapses many proofs into a single simp_all.", + "assessment": { + "scope": "proof golf", + "introduces_tech_debt": True, + "maintainability": "regressed", + "brittleness": "more_brittle", + "risk": "medium", + "assessment_one_sentence": "Shorter, but more fragile.", + }, + "verdict": "needs_discussion", + "findings": [], + }, + model="gpt-5.5", + usage=None, + tier="flex", + reviewed_head_sha="deadbeef", + kind="refactor", + ) + + assert body.startswith(LLM_REVIEW_MARKER) + assert "LLM review — refactor" in body + assert "Brittleness" in body + assert "Introduces tech debt" in body + assert "REFACTOR_REVIEW_RULES.md" in body + # Project-only assessment fields must not leak into a refactor review. + assert "| Fit |" not in body + assert "| Level |" not in body diff --git a/python/tests/test_statements.py b/python/tests/test_statements.py new file mode 100644 index 0000000000..b504947f6f --- /dev/null +++ b/python/tests/test_statements.py @@ -0,0 +1,130 @@ +"""Tests for the statement-change parser used by the proof profile. + +``scripts/proof-profile/statements.py`` is fetched and run standalone in CI, +so it lives outside the ``lean_pool`` package; add its directory to the path +before importing it. +""" + +from __future__ import annotations + +import pathlib +import sys + +SCRIPTS = pathlib.Path(__file__).resolve().parents[2] / "scripts" / "proof-profile" +sys.path.insert(0, str(SCRIPTS)) + +import statements # noqa: E402 + +BASE = """ +namespace Foo + +theorem add_comm' (a b : Nat) : a + b = b + a := by + have h : a + b = b + a := Nat.add_comm a b + exact h + +def double (n : Nat) : Nat := n + n + +lemma embedded : (⟨1, by simp⟩ : {n : Nat // n = 1}).1 = 1 := by rfl + +end Foo +""" + + +def test_pure_golf_changes_no_statement() -> None: + """Golfing proofs and definition bodies is not a statement change.""" + head = """ +namespace Foo + +theorem add_comm' (a b : Nat) : a + b = b + a := by + simp_all [Nat.add_comm] + +def double (n : Nat) : Nat := 2 * n + +lemma embedded : (⟨1, by omega⟩ : {n : Nat // n = 1}).1 = 1 := by rfl + +end Foo +""" + diff = statements.compare_statements(BASE, head) + assert diff.statement_changed == [] + assert diff.binder_renamed == [] + assert diff.added == [] + assert diff.removed == [] + assert diff.head_decl_count == 3 + + +def test_real_type_change_is_flagged() -> None: + """Changing a declaration's type counts as a statement change.""" + head = BASE.replace( + "def double (n : Nat) : Nat := n + n", + "def double (n : Int) : Int := n + n", + ) + diff = statements.compare_statements(BASE, head) + assert diff.statement_changed == ["Foo.double"] + assert diff.binder_renamed == [] + + +def test_underscore_binder_rename_is_not_a_statement_change() -> None: + """Marking a hypothesis unused (`h` -> `_h`) preserves the proposition.""" + base = """ +theorem t (a b : Nat) (h : 0 < b) : a + 0 = a := by + rw [Nat.add_zero] +""" + head = """ +theorem t (a b : Nat) (_h : 0 < b) : a + 0 = a := by + simp +""" + diff = statements.compare_statements(base, head) + assert diff.statement_changed == [] + assert diff.binder_renamed == ["t"] + + +def test_added_and_removed_declarations() -> None: + """Declarations gained or lost are reported separately.""" + head = """ +namespace Foo + +theorem add_comm' (a b : Nat) : a + b = b + a := by simp_all + +def double (n : Nat) : Nat := n + n + +theorem brand_new : True := trivial + +end Foo +""" + diff = statements.compare_statements(BASE, head) + assert diff.statement_changed == [] + assert diff.added == ["Foo.brand_new"] + assert diff.removed == ["Foo.embedded"] + + +def test_leading_absolute_value_bar_is_not_an_arm() -> None: + """A line-leading `|x| ≤ …` in the type must not truncate the signature. + + Regression: `|…|` at line start was misread as an equation-compiler arm + when the proof contained a `=>`, so golfing the proof (adding a `fun … =>`) + produced a spurious statement change even though the type was identical. + """ + base = """ +lemma bound (f : Nat → Real) (h : 0 < 1) : + ∃ C : Real, ∀ n, + |Real.log (f n)| ≤ C := by + intro n + exact something n +""" + head = """ +lemma bound (f : Nat → Real) (h : 0 < 1) : + ∃ C : Real, ∀ n, + |Real.log (f n)| ≤ C := + fun n => something n +""" + diff = statements.compare_statements(base, head) + assert diff.statement_changed == [] + assert diff.binder_renamed == [] + + +def test_identical_source_is_noop() -> None: + """Comparing a file against itself reports nothing.""" + diff = statements.compare_statements(BASE, BASE) + assert diff.statement_changed == [] + assert diff.added == [] + assert diff.removed == [] diff --git a/scripts/proof-profile/render.py b/scripts/proof-profile/render.py index 4db583467a..a856737035 100644 --- a/scripts/proof-profile/render.py +++ b/scripts/proof-profile/render.py @@ -13,6 +13,14 @@ import subprocess from pathlib import Path +# statements.py is fetched from origin/main alongside this script (see the +# report job in proof-profile.yml). Import defensively so an older cached +# workflow that has not fetched it yet still renders the rest of the profile. +try: + import statements as statements_mod +except ImportError: # pragma: no cover - only when the fetch step is missing + statements_mod = None + log_path = Path("proof-profile.log") heartbeat_log_path = Path("proof-profile-heartbeats.log") base_heartbeat_log_path = Path("proof-profile-base-heartbeats.log") @@ -202,6 +210,52 @@ def changed_line_stats(files: list[str]) -> dict[str, tuple[int, int]]: return stats +def git_show(ref: str, path: str) -> str | None: + """Return a file's contents at ``ref``, or ``None`` if it is absent.""" + + try: + return subprocess.check_output( + ["git", "show", f"{ref}:{path}"], + text=True, + stderr=subprocess.DEVNULL, + ) + except subprocess.CalledProcessError: + return None + + +def statement_changes(files: list[str]) -> dict[str, "statements_mod.StatementDiff"]: + """Map each modified file to its base→head statement diff. + + Compares against the merge base (what the PR actually changed) using the + same textual parser physlib's `/check-golf` uses; no build is needed. + Files that cannot be read on either side are skipped. + """ + + if statements_mod is None or not files: + return {} + base_sha = os.environ.get("BASE_SHA") + head_sha = os.environ.get("HEAD_SHA", "HEAD") + if not base_sha: + return {} + try: + merge_base = subprocess.check_output( + ["git", "merge-base", base_sha, head_sha], + text=True, + stderr=subprocess.DEVNULL, + ).strip() + except subprocess.CalledProcessError: + merge_base = "" + base_ref = merge_base or base_sha + result: dict[str, statements_mod.StatementDiff] = {} + for path in files: + base_src = git_show(base_ref, path) + head_src = git_show(head_sha, path) + if base_src is None or head_src is None: + continue + result[path] = statements_mod.compare_statements(base_src, head_src) + return result + + added_files = os.environ.get("ADDED_FILES", "").split() modified_files = os.environ.get("MODIFIED_FILES", "").split() compare = os.environ.get("COMPARE", "") == "true" @@ -696,6 +750,101 @@ def comparison_section(cap: int | None) -> list[str]: ) +# --------------------------------------------------------------------------- +# Statement-change section: for every modified file, report whether any +# declaration changed its *statement* (signature / type) rather than only its +# proof or definition body — the reassurance a maintainer wants from a +# refactor ("no theorem was quietly restated"). Independent of the heartbeat +# comparison (pure text, no build), so it renders even when the compare was +# skipped. Absent for new-project PRs, which have no modified files. +# --------------------------------------------------------------------------- +STATEMENT_LIST_CAP = 50 +statement_diffs = statement_changes(modified_files) + + +def build_statement_section(cap: int | None) -> list[str]: + """Render the statement-change subsection; empty when nothing to say.""" + + if not statement_diffs: + return [] + changed = [ + (p, n) for p, d in statement_diffs.items() for n in d.statement_changed + ] + renamed = [ + (p, n) for p, d in statement_diffs.items() for n in d.binder_renamed + ] + added = [(p, n) for p, d in statement_diffs.items() for n in d.added] + removed = [(p, n) for p, d in statement_diffs.items() for n in d.removed] + total_decls = sum(d.head_decl_count for d in statement_diffs.values()) + n_files = len(statement_diffs) + changed_files = len({p for p, _ in changed}) + + s = ["### Statement changes\n\n"] + if changed: + s.append( + f"⚠️ **{format_int(len(changed))} declaration" + f"{'' if len(changed) == 1 else 's'} changed their statement** " + f"across {format_int(changed_files)} file" + f"{'' if changed_files == 1 else 's'} — a statement change is more " + "than a refactor. Confirm each one is intended.\n\n" + ) + else: + s.append( + f"✅ **No statements changed** — all {format_int(total_decls)} " + f"tracked declaration{'' if total_decls == 1 else 's'} across " + f"{format_int(n_files)} modified file{'' if n_files == 1 else 's'} " + "kept their type; only proofs / definition bodies " + f"{'(and binder names) ' if renamed else ''}changed.\n\n" + ) + + def detail_block(title: str, items: list[tuple[str, str]], open_: bool) -> None: + if not items: + return + shown = items if cap is None else items[:cap] + s.append( + f"{title} " + f"({format_int(len(items))})\n\n" + ) + for path, name in sorted(shown): + s.append(f"- `{name}` — `{path}`\n") + if cap is not None and len(items) > cap: + s.append(f"- _… +{format_int(len(items) - cap)} more_\n") + s.append("\n\n\n") + + detail_block("⚠️ Statements changed", changed, open_=True) + if renamed: + s.append( + f"_{format_int(len(renamed))} declaration" + f"{'' if len(renamed) == 1 else 's'} had only a binder renamed " + "(most often a hypothesis marked unused as `_h…`); the proposition " + "is unchanged, so these are not statement changes._\n\n" + ) + detail_block("✍️ Binder renamed (proposition unchanged)", renamed, open_=False) + if added or removed: + s.append( + f"_Also: {format_int(len(added))} declaration" + f"{'' if len(added) == 1 else 's'} added, " + f"{format_int(len(removed))} removed. A reorganization moves " + "declarations between files, which shows up here as an add in one " + "file and a remove in another._\n\n" + ) + detail_block("➕ Declarations added", added, open_=False) + detail_block("➖ Declarations removed", removed, open_=False) + + s.append( + "_Statements are compared textually against the merge base (comments " + "and whitespace ignored; `by` proof terms embedded in a type are " + "treated as proof-irrelevant), the same method as physlib's " + "`/check-golf`. Anonymous instances and `example`s are not tracked._" + "\n\n" + ) + return s + + +statement_out_full = build_statement_section(None) +statement_out_capped = build_statement_section(STATEMENT_LIST_CAP) + + def bound_comment(text, limit): """Trim a rendered profile to fit GitHub's comment size cap. @@ -766,9 +915,11 @@ def assemble(n): return out_text -rendered_full = "".join(out + comparison_full + absolute_out + out_comment_extra) +rendered_full = "".join( + out + statement_out_full + comparison_full + absolute_out + out_comment_extra +) rendered_comment = "".join( - out + comparison_capped + absolute_out + out_comment_extra + out + statement_out_capped + comparison_capped + absolute_out + out_comment_extra ) # The full render always goes to the job step summary (~1 MB limit) diff --git a/scripts/proof-profile/statements.py b/scripts/proof-profile/statements.py new file mode 100644 index 0000000000..c89ff4518a --- /dev/null +++ b/scripts/proof-profile/statements.py @@ -0,0 +1,451 @@ +"""Textual detection of Lean *statement* changes between two file revisions. + +Fetched from origin/main and imported by +``.github/workflows/proof-profile.yml``'s render step so the proof profile +can report, for a refactor PR, whether any declaration changed its +*statement* (its signature: name, binders, and type) rather than only its +proof or definition body. That is the "did this golf touch a theorem?" +question — the reassurance a maintainer wants from a refactor. + +The approach is the same as physlib's ``check_golf.py``: parse each side +textually — no Lean build — by stripping comments and string literals, +tracking bracket depth, and splitting each declaration at the top-level +``:=`` / ``where`` that separates its statement from its body. Proof terms +embedded inside a *type* (``⟨x, by omega⟩``, ``(by decide)``) are masked so +that golfing them is not mistaken for a statement change (they are +proof-irrelevant). Only stdlib is used, because this module is fetched and +run standalone in CI, not installed as part of the ``lean_pool`` package. +""" + +from __future__ import annotations + +import re +from dataclasses import dataclass + +# Keywords that introduce a named declaration whose statement we track. +DECL_KEYWORDS = ( + "theorem", + "lemma", + "def", + "abbrev", + "instance", + "example", + "structure", + "inductive", + "class", + "opaque", +) + +# Modifiers that may sit between the line start and the declaration keyword +# (``@[...]`` attributes and ``set_option ... in`` / ``open ... in`` prefixes +# are handled structurally, not through this set). +MODIFIERS = { + "private", + "protected", + "noncomputable", + "unsafe", + "partial", + "nonrec", + "scoped", + "local", + "mutual", +} + +# Keywords that open/close a namespacing scope. +SCOPE_KEYWORDS = {"namespace", "section", "end"} + +OPEN_BRACKETS = "([{⟨⦃" +CLOSE_BRACKETS = ")]}⟩⦄" + +# Characters that terminate the name token following a declaration keyword. +NAME_STOP = set(" \t\r\n({[⦃⟨:=") + + +# --------------------------------------------------------------------------- # +# Lean lexical pre-processing +# --------------------------------------------------------------------------- # +def code_view(text: str) -> str: + """Return ``text`` with comments and string literals blanked to spaces. + + Length and newline positions are preserved so indices computed on the + result line up with the original source. Block comments (``/- -/``) nest, + which also covers doc comments (``/-- -/``) and module docs (``/-! -/``). + """ + out: list[str] = [] + i, n = 0, len(text) + NORMAL, LINE, BLOCK, STR = 0, 1, 2, 3 + state = NORMAL + block_depth = 0 + while i < n: + c = text[i] + two = text[i : i + 2] + if state == NORMAL: + if two == "--": + out.append(" ") + i += 2 + state = LINE + continue + if two == "/-": + out.append(" ") + i += 2 + state = BLOCK + block_depth = 1 + continue + if c == '"': + out.append(" ") + i += 1 + state = STR + continue + out.append(c) + i += 1 + elif state == LINE: + if c == "\n": + out.append("\n") + state = NORMAL + else: + out.append(" ") + i += 1 + elif state == BLOCK: + if two == "/-": + out.append(" ") + i += 2 + block_depth += 1 + continue + if two == "-/": + out.append(" ") + i += 2 + block_depth -= 1 + if block_depth == 0: + state = NORMAL + continue + out.append("\n" if c == "\n" else " ") + i += 1 + else: # STR + if c == "\\": + out.append(" " if i + 1 < n else " ") + i += 2 + continue + if c == '"': + out.append(" ") + state = NORMAL + i += 1 + continue + out.append("\n" if c == "\n" else " ") + i += 1 + return "".join(out) + + +def normalize(fragment: str) -> str: + """Collapse whitespace so pure reformatting is not seen as a change.""" + return " ".join(fragment.split()) + + +# A leading underscore run at the start of an identifier token — the marker a +# golf adds to a binder that its shorter proof no longer uses (`hM` -> `_hM`). +_LEADING_UNDERSCORE_RE = re.compile(r"(? str: + """Drop leading underscores from identifier tokens in a signature. + + Renaming a binder to a ``_``-prefixed name (to mark it unused) is the one + signature edit a golf routinely makes, and it does *not* change the + proposition: binder names are alpha-equivalent, so ``∀ (hM : p), q`` and + ``∀ (_hM : p), q`` are the same type. Stripping the leading underscores + lets us tell such a rename apart from a genuine change to the type. + """ + return _LEADING_UNDERSCORE_RE.sub("", signature) + + +def _ident_char(c: str) -> bool: + return c.isalnum() or c in "_.'" or ord(c) > 127 + + +def mask_by_blocks(sig_code: str) -> str: + """Blank the contents of ``by`` tactic blocks embedded inside a statement. + + A statement's *type* can embed proof terms — ``⟨x, by omega⟩`` or an + argument such as ``(by decide)``. By proof irrelevance those tactic + blocks do not affect the elaborated type, so golfing them keeps the + statement. Each embedded ``by`` block runs to the end of its enclosing + bracket group; we replace it with a placeholder so signatures that + differ only inside such blocks compare equal. + """ + out: list[str] = [] + i, n = 0, len(sig_code) + depth = 0 + while i < n: + if ( + sig_code[i : i + 2] == "by" + and (i == 0 or not _ident_char(sig_code[i - 1])) + and (i + 2 >= n or not _ident_char(sig_code[i + 2])) + ): + d0 = depth + out.append("by<>") + i += 2 + while i < n: + c = sig_code[i] + if c in OPEN_BRACKETS: + depth += 1 + elif c in CLOSE_BRACKETS: + if depth == d0: + break # close bracket of the enclosing group + depth -= 1 + i += 1 + continue + c = sig_code[i] + if c in OPEN_BRACKETS: + depth += 1 + elif c in CLOSE_BRACKETS: + depth = max(0, depth - 1) + out.append(c) + i += 1 + return normalize("".join(out)) + + +# --------------------------------------------------------------------------- # +# Declaration extraction +# --------------------------------------------------------------------------- # +@dataclass +class Decl: + """A named declaration and its statement (the part before the body).""" + + name: str + keyword: str + signature: str # normalized statement (keyword .. up to `:=` / `where`) + signature_masked: str # same, with embedded `by` proof blocks blanked + + +def _line_prefix(code: str, pos: int) -> str: + """The text on ``pos``'s line, up to ``pos`` (from the previous newline).""" + start = code.rfind("\n", 0, pos) + 1 + return code[start:pos] + + +_WHERE_RE = re.compile(r"(? list[int]: + """Indices of top-level command starts: non-blank characters in column 0. + + In Mathlib-style Lean, top-level commands (``lemma``, ``def``, + ``namespace``, ...) begin in column 0, while everything that belongs to a + command — multi-line signatures, tactic blocks, term proofs — is + indented. Segmenting on column-0 lines is robust even when a proof body + contains brackets we cannot balance textually. + """ + starts = [0] if code and not code[0].isspace() else [] + for i in range(1, len(code)): + if code[i - 1] == "\n" and not code[i].isspace() and code[i] != "\n": + starts.append(i) + return starts + + +def _read_token(code: str, pos: int, end: int) -> str: + j = pos + while j < end and code[j] not in NAME_STOP and code[j] != "@": + j += 1 + return code[pos:j] + + +def _strip_prefixes(code: str, start: int, end: int) -> int: + """Skip attributes / modifiers / ``... in`` prefixes; return keyword index.""" + pos = start + while pos < end: + while pos < end and code[pos] in " \t\r\n": + pos += 1 + if pos >= end: + break + if code[pos] == "@" and pos + 1 < end and code[pos + 1] == "[": + depth = 0 + while pos < end: + if code[pos] == "[": + depth += 1 + elif code[pos] == "]": + depth -= 1 + if depth == 0: + pos += 1 + break + pos += 1 + continue + tok = _read_token(code, pos, end) + if tok in MODIFIERS: + pos += len(tok) + continue + if tok in ("set_option", "open"): + m = re.compile(r"(? int: + """Index in ``[start, end)`` where the statement ends and the body begins. + + Bracket depth is tracked *locally* to this declaration. The body begins + at the first top-level ``:=`` or ``where``, or — for equation-compiler + declarations that have neither — at the first line-leading ``|`` arm + (recognised by a following top-level ``=>``, which distinguishes a real + arm from an absolute value ``|x|`` in a type). Returns ``end`` if none. + """ + b_assign = b_where = b_bar = None + seen_bars: list[int] = [] + depth = 0 + i = start + while i < end: + c = code[i] + if depth == 0: + if b_assign is None and code[i : i + 2] == ":=": + b_assign = i + elif ( + code[i : i + 2] == "=>" + and seen_bars + and b_bar is None + and b_assign is None + and b_where is None + ): + # A line-leading `|` is an equation-compiler arm only if its + # `=>` arrives before any top-level `:=`/`where`. This keeps an + # absolute-value bar in the type (`|x| ≤ ε`) from being read as + # an arm — its nearest `=>` is inside the proof, after the `:=` + # — while still catching a genuine `def f : T | p => e` (whose + # arm `=>` precedes any `:=` sitting inside a later arm body). + b_bar = seen_bars[0] + elif b_where is None and _WHERE_RE.match(code, i): + b_where = i + if c == "|" and _line_prefix(code, i).strip() == "": + seen_bars.append(i) + if c in OPEN_BRACKETS: + depth += 1 + elif c in CLOSE_BRACKETS: + depth = max(0, depth - 1) + i += 1 + candidates = [b for b in (b_assign, b_where, b_bar) if b is not None] + return min(candidates) if candidates else end + + +def _apply_scope(stack: list[tuple[str, str]], keyword: str, name: str) -> None: + if keyword == "namespace": + stack.append(("namespace", name)) + elif keyword == "section": + stack.append(("section", name)) + else: # end + if name: + for k in range(len(stack) - 1, -1, -1): + if stack[k][1] == name: + del stack[k:] + return + if stack: + stack.pop() + elif stack: + stack.pop() + + +def parse_decls(text: str) -> dict[str, Decl]: + """Parse ``text`` into a map from qualified name to :class:`Decl`.""" + code = code_view(text) + starts = _block_starts(code) + ns_stack: list[tuple[str, str]] = [] + result: dict[str, Decl] = {} + seen: dict[str, int] = {} + + for idx, start in enumerate(starts): + end = starts[idx + 1] if idx + 1 < len(starts) else len(code) + kw_pos = _strip_prefixes(code, start, end) + keyword = _read_token(code, kw_pos, end) + + if keyword in SCOPE_KEYWORDS: + rest = code[kw_pos + len(keyword) : end].split("\n", 1)[0].strip() + name = rest.split()[0] if rest else "" + _apply_scope(ns_stack, keyword, name) + continue + if keyword not in DECL_KEYWORDS: + continue + + # Parse the declaration name. + j = kw_pos + len(keyword) + while j < end and code[j] in " \t\r\n": + j += 1 + k = j + while k < end and code[k] not in NAME_STOP: + k += 1 + local = code[j:k] + if not local: + continue # anonymous instance / example — cannot track by name + + boundary = _find_boundary(code, k, end) + sig_code = code[kw_pos:boundary] + signature = normalize(sig_code) + signature_masked = mask_by_blocks(sig_code) + + prefix = ".".join( + nm for kind, nm in ns_stack if kind == "namespace" and nm + ) + qualified = (prefix + "." + local) if prefix else local + if qualified in seen: + seen[qualified] += 1 + qualified = f"{qualified}#{seen[qualified]}" + else: + seen[qualified] = 0 + result[qualified] = Decl(qualified, keyword, signature, signature_masked) + return result + + +# --------------------------------------------------------------------------- # +# Comparison +# --------------------------------------------------------------------------- # +@dataclass +class StatementDiff: + """Which declarations changed statement between two revisions of a file.""" + + statement_changed: list[str] # signature (type) genuinely changed + binder_renamed: list[str] # only binder names differ; proposition unchanged + added: list[str] # declarations new in head + removed: list[str] # declarations gone from head + head_decl_count: int # named declarations in the head revision + + +def compare_statements(base_src: str, head_src: str) -> StatementDiff: + """Compare two revisions of a file and classify statement changes. + + A declaration counts as ``statement_changed`` only when the elaborated + *type* really changed. Signature edits that leave the proposition intact + are excluded: golfing a ``by`` proof term embedded in the type + (proof-irrelevant), and renaming a binder — most often to a ``_``-prefixed + unused marker — which is reported separately as ``binder_renamed``. + Golfing a proof or a definition body (type preserved) is not a statement + change at all. + """ + base = parse_decls(base_src) + head = parse_decls(head_src) + statement_changed: list[str] = [] + binder_renamed: list[str] = [] + added: list[str] = [] + removed: list[str] = [] + for name, d in head.items(): + b = base.get(name) + if b is None: + added.append(name) + continue + if b.signature == d.signature: + continue + if b.signature_masked == d.signature_masked: + continue # only an embedded `by` proof term differs; type unchanged + if ignore_underscore_binders(b.signature_masked) == ignore_underscore_binders( + d.signature_masked + ): + binder_renamed.append(name) # only a `_`-binder rename; type unchanged + else: + statement_changed.append(name) + for name in base: + if name not in head: + removed.append(name) + return StatementDiff( + statement_changed=statement_changed, + binder_renamed=binder_renamed, + added=added, + removed=removed, + head_decl_count=len(head), + )