Make /review and /profile refactor-aware

.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": "<one short paragraph: what this refactor changes and how, in plain language>",
+  "assessment": {
+    "scope": "<one short phrase: e.g. 'proof golf', 'module split', 'API rename', 'tactic rewrite'>",
+    "introduces_tech_debt": <bool: true iff the refactor leaves at least one proof/definition harder to maintain or more brittle than before>,
+    "maintainability": "improved" | "unchanged" | "regressed",
+    "brittleness": "more_robust" | "unchanged" | "more_brittle",
+    "risk": "low" | "medium" | "high",
+    "assessment_one_sentence": "<one sentence: the bottom line for the maintainer>"
+  },
+  "verdict": "approve" | "request_changes" | "needs_discussion",
+  "findings": [
+    {
+      "file": "<repo-relative path, or empty if PR-wide>",
+      "line": <int, post-change line; 0 if not file-specific>,
+      "rule": "<short tag, e.g. 'brittle-automation', 'lost-structure', 'perf-regression', 'reusability-lost', 'dead-leftover'>",
+      "comment": "<one short paragraph: what's wrong, where, concrete suggestion>"
+    }
+  ]
+}
+```
+
+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.

.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
 

.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