feat: keep the previous Lean declarations diff visible while a new build runs

scripts/pr_summary/updateDeclsDiffSection.py

@@ -20,14 +20,23 @@
                       `declsDiff.py --with-heading`
     DEFAULT_BRANCH  warning mode: branch named in the rebase hint (default `master`)
 
-Modes (both replace the Lean region wholesale):
-    success — the rendered Lean-aware section (heading `(Lean)`).
-    warning — a cache-miss block (heading `(Lean -- unavailable)`); the regex
-              block elsewhere in the comment stays visible.
+Modes:
+    success — splice in the rendered Lean-aware section (heading `(Lean)`).
+    warning — cache miss. If the comment already shows a real Lean diff, carry it
+              forward under `NEW_HEADING` (keeping the diff visible); otherwise
+              splice a cache-miss block (heading `(Lean -- unavailable)`).
+    emit    — pre-build helper. Does NOT patch: prints the Lean region content
+              (no markers) to stdout for `mathlib4`'s `PR_summary.yml` to embed.
+              Carries the existing real diff forward under `NEW_HEADING`, else
+              prints the pending placeholder.
+
+A "real diff" is recognised by its body stamp (`✅ **Lean-aware diff**`), not its
+heading, so a once-shown diff survives repeated relabels (stale → cache miss → …)
+without ever reverting to the pending placeholder.
 
 Exit codes:
-    0 — patched, or nothing to do (no summary comment / no markers / unchanged)
-    1 — non-recoverable error (gh CLI failure, malformed env)
+    0 — patched / emitted, or nothing to do (no summary comment / no markers / unchanged)
+    1 — non-recoverable error (gh CLI failure, malformed env); `emit` never returns 1
 """
 
 from __future__ import annotations
@@ -42,22 +51,78 @@
 LEAN_BEGIN = "<!-- DECLS_DIFF_LEAN_BEGIN -->"
 LEAN_END = "<!-- DECLS_DIFF_LEAN_END -->"
 PR_SUMMARY_PREFIX = "### PR summary"
+# The summary comment is posted/patched by `update_PR_comment.sh` with the
+# default `GITHUB_TOKEN`, so it is always authored by this account.
+SUMMARY_COMMENT_AUTHOR = "github-actions[bot]"
 
 _REGION_RE = re.compile(re.escape(LEAN_BEGIN) + r"(.*?)" + re.escape(LEAN_END), re.DOTALL)
 
+# A real Lean diff is identified by this body stamp (emitted by `declsDiff.py`),
+# which survives heading relabels — unlike the heading, which changes each time.
+LEAN_DIFF_STAMP = "✅ **Lean-aware diff**"
+# Matches the heading line in any of its states: `(Lean)`, `(Lean -- pending)`,
+# `(Lean -- stale ...)`, `(Lean -- cache miss ...)`, `(Lean -- unavailable)`.
+_HEADING_RE = re.compile(r"(?m)^#### Declarations diff \(Lean[^\n]*\)$")
+
+PENDING_PLACEHOLDER = (
+    "#### Declarations diff (Lean -- pending)\n\n"
+    "_Computed after the build finishes._"
+)
+
 
 def build_warning(default_branch: str) -> str:
     """Render the cache-miss block that replaces the Lean region on a miss.
     The heading carries the `(Lean -- unavailable)` status."""
     return "\n".join([
         "#### Declarations diff (Lean -- unavailable)",
         "",
-        f"> ⚠️ The Mathlib cache for this PR's merge-base isn't on the server "
-        f"(typically a bors-batch intermediate that CI never built). "
-        f"Merge `{default_branch}` into this PR and push to refresh.",
+        f"> ⚠️ No declarations diff yet: there is no built `{default_branch}` snapshot "
+        f"at this PR's merge-base (typically a bors-batch intermediate that CI never "
+        f"built). Merge `{default_branch}` into this PR and push to refresh.",
     ])
 
 
+def carry_forward(region: str, new_heading: str) -> str | None:
+    """If `region` holds a real Lean-aware diff (identified by its body stamp,
+    not its heading — so it survives repeated relabels), return that region with
+    the heading line rewritten to `new_heading`. Otherwise return `None`."""
+    if not new_heading or LEAN_DIFF_STAMP not in region:
+        return None
+    # Substitute `new_heading` literally (via a lambda), NOT as a regex
+    # replacement template, so a heading containing `\` or `\g` cannot corrupt it.
+    relabelled, n = _HEADING_RE.subn(lambda _m: new_heading.strip(), region, count=1)
+    if n == 0:
+        # Stamp present but no `(Lean…)` heading matched: a NEW_HEADING was added
+        # that `_HEADING_RE` doesn't recognise. Carry the body forward unrelabelled
+        # rather than silently no-op, and make the drift visible in the logs.
+        print("updateDeclsDiffSection: carry_forward: diff stamp present but no "
+              "'#### Declarations diff (Lean…)' heading matched; check _HEADING_RE "
+              "against the NEW_HEADING values.", file=sys.stderr)
+    return relabelled.strip()
+
+
+def emit_placeholder(repo: str, head_sha: str) -> int:
+    """`MODE=emit`: print the Lean region content for the pre-build to embed (it
+    never patches and never fails the caller). Carry the existing real diff
+    forward under `NEW_HEADING` when one exists, else print the pending
+    placeholder."""
+    new_heading = os.environ.get("NEW_HEADING", "")
+    carried = None
+    try:
+        pr = resolve_pr(repo, head_sha)
+        if pr is not None:
+            comments = gh_json("--paginate", f"repos/{repo}/issues/{pr}/comments")
+            target = find_summary_comment(comments)
+            if target is not None:
+                m = _REGION_RE.search(target.get("body") or "")
+                if m is not None:
+                    carried = carry_forward(m.group(1), new_heading)
+    except subprocess.CalledProcessError as e:
+        print(f"updateDeclsDiffSection: gh api failed: {e.stderr}", file=sys.stderr)
+    sys.stdout.write(carried if carried is not None else PENDING_PLACEHOLDER)
+    return 0
+
+
 def splice(body: str, block: str) -> str:
     """Replace the Lean-marked region's content with `block`. Returns `body`
     unchanged when the markers are absent. Idempotent for a given `block`."""
@@ -68,11 +133,18 @@ def splice(body: str, block: str) -> str:
 
 
 def find_summary_comment(comments: list[dict]) -> dict | None:
-    """Return the first comment whose body starts with `### PR summary`, else
-    `None`. Tolerates a `null` body (the GitHub API permits it) by treating it
-    as empty rather than raising."""
+    """Return the first `github-actions[bot]` comment whose body starts with
+    `### PR summary`, else `None`. Tolerates a `null` body (the GitHub API
+    permits it) by treating it as empty rather than raising.
+
+    The author check matters: anyone can post a comment starting with
+    `### PR summary`, and under `pull_request_target` this script reads that
+    comment's Lean region and carries it forward into the comment it maintains.
+    Requiring the bot author keeps attacker-authored content out of that loop."""
     return next(
-        (c for c in comments if (c.get("body") or "").startswith(PR_SUMMARY_PREFIX)),
+        (c for c in comments
+         if (c.get("body") or "").startswith(PR_SUMMARY_PREFIX)
+         and (c.get("user") or {}).get("login") == SUMMARY_COMMENT_AUTHOR),
         None,
     )
 
@@ -115,6 +187,11 @@ def main() -> int:
     head_sha = os.environ.get("PR_HEAD_SHA", "")
     mode = os.environ.get("MODE", "success")
 
+    # `emit` is a self-contained, non-patching path: handle it before the
+    # patch flow below so that path stays byte-for-byte unchanged.
+    if mode == "emit":
+        return emit_placeholder(repo, head_sha)
+
     try:
         pr = resolve_pr(repo, head_sha)
     except subprocess.CalledProcessError as e:
@@ -138,7 +215,12 @@ def main() -> int:
         return 0
 
     if mode == "warning":
-        block = build_warning(os.environ.get("DEFAULT_BRANCH", "master"))
+        # Keep a previously-shown real diff visible across a cache miss, with the
+        # heading surfacing the miss; only fall back to the unavailable block when
+        # there is no prior diff to carry forward.
+        m = _REGION_RE.search(target.get("body") or "")
+        block = (m and carry_forward(m.group(1), os.environ.get("NEW_HEADING", ""))) \
+            or build_warning(os.environ.get("DEFAULT_BRANCH", "master"))
     else:
         override = os.environ.get("OVERRIDE_FILE", "")
         block = Path(override).read_text() if override and Path(override).is_file() else ""

tests/decls_diff/test_patch.py

@@ -2,18 +2,27 @@
 
 from __future__ import annotations
 
+from declsDiff import render_override
 from updateDeclsDiffSection import (
     LEAN_BEGIN,
     LEAN_END,
     PR_SUMMARY_PREFIX,
+    SUMMARY_COMMENT_AUTHOR,
     build_warning,
+    carry_forward,
     find_summary_comment,
     splice,
 )
 
+BOT = {"login": SUMMARY_COMMENT_AUTHOR}
+HUMAN = {"login": "not-the-bot"}
+
 # A success block as produced by `declsDiff.py --with-heading`.
 SECTION = "#### Declarations diff (Lean)\n\n> ✅ **Lean-aware diff**\n\n* **+1** new declarations\n"
 
+STALE_HEADING = "#### Declarations diff (Lean -- stale, waiting for the new build)"
+MISS_HEADING = "#### Declarations diff (Lean -- stale; merge master and push to refresh)"
+
 
 def comment(inner: str) -> str:
     """A minimal `### PR summary` comment carrying the regex block plus a Lean
@@ -80,24 +89,100 @@ def test_summary_prefix_preserved(self) -> None:
         assert splice(comment(PLACEHOLDER), build_warning("master")).startswith(PR_SUMMARY_PREFIX)
 
 
+class TestCarryForward:
+    def test_real_diff_relabelled_body_kept(self) -> None:
+        """A real diff is carried forward: heading swapped, stamp and counts kept."""
+        out = carry_forward(SECTION, STALE_HEADING)
+        assert out is not None
+        assert out.startswith(STALE_HEADING)
+        assert "✅ **Lean-aware diff**" in out
+        assert "**+1** new declarations" in out
+        assert "(Lean -- pending)" not in out
+
+    def test_survives_repeated_relabels(self) -> None:
+        """Keyed on the body stamp (not the heading), so a stale diff can be
+        relabelled again (e.g. on a later cache miss) without being lost."""
+        stale = carry_forward(SECTION, STALE_HEADING)
+        miss = carry_forward(stale, MISS_HEADING)
+        assert miss is not None
+        assert miss.startswith(MISS_HEADING)
+        assert "**+1** new declarations" in miss
+
+    def test_pending_not_carryable(self) -> None:
+        """The pending placeholder has no diff stamp, so there is nothing to keep."""
+        assert carry_forward(PLACEHOLDER, STALE_HEADING) is None
+
+    def test_empty_heading_never_carries(self) -> None:
+        assert carry_forward(SECTION, "") is None
+
+    def test_warning_keeps_prior_diff(self) -> None:
+        """Warning mode carries a prior real diff forward under the cache-miss
+        heading instead of blanking it to `unavailable`."""
+        prior = splice(comment(PLACEHOLDER), SECTION)
+        kept = carry_forward(SECTION, MISS_HEADING)
+        assert kept is not None
+        body = splice(prior, kept)
+        assert MISS_HEADING in body
+        assert "**+1** new declarations" in body
+        assert "(Lean -- unavailable)" not in body
+
+    def test_warning_falls_back_when_no_prior_diff(self) -> None:
+        """With only the pending placeholder present, warning mode still shows
+        the unavailable block."""
+        assert carry_forward(PLACEHOLDER, MISS_HEADING) is None
+        body = splice(comment(PLACEHOLDER), build_warning("master"))
+        assert "(Lean -- unavailable)" in body
+
+    def test_real_producer_output_is_carryable(self) -> None:
+        """Contract guard against stamp drift: a section rendered by the *real*
+        producer (`render_override`, the same code path the post-build action
+        runs) must satisfy `carry_forward`. The hand-written `SECTION` fixture
+        cannot catch a reworded stamp in declsDiff.py — this can."""
+        produced = render_override(
+            plus=1, minus=0, diff=[("+", "Foo.bar")],
+            head_sha="abc1234def", with_heading=True,
+        )
+        assert carry_forward(produced, STALE_HEADING) is not None
+
+    def test_heading_with_regex_metachars_is_literal(self) -> None:
+        """A heading containing backslashes is substituted literally, not as a
+        regex replacement template."""
+        out = carry_forward(SECTION, r"#### Declarations diff (Lean \g<0> \1)")
+        assert r"\g<0>" in out
+
+
 class TestFindSummaryComment:
     def test_finds_the_summary_among_others(self) -> None:
-        """The `### PR summary` comment is picked out of a list of comments."""
+        """The bot's `### PR summary` comment is picked out of a list of comments."""
         comments = [
-            {"body": "a normal review comment"},
-            {"body": f"{PR_SUMMARY_PREFIX} [abc](url)\n\nbody"},
-            {"body": "another comment"},
+            {"body": "a normal review comment", "user": HUMAN},
+            {"body": f"{PR_SUMMARY_PREFIX} [abc](url)\n\nbody", "user": BOT},
+            {"body": "another comment", "user": HUMAN},
         ]
         assert find_summary_comment(comments)["body"].startswith(PR_SUMMARY_PREFIX)
 
     def test_returns_none_when_absent(self) -> None:
-        assert find_summary_comment([{"body": "nope"}]) is None
+        assert find_summary_comment([{"body": "nope", "user": BOT}]) is None
         assert find_summary_comment([]) is None
 
     def test_tolerates_null_body(self) -> None:
         """A comment with a `null` body (allowed by the API) is skipped, not fatal."""
         comments = [
-            {"body": None},
-            {"body": f"{PR_SUMMARY_PREFIX}\n\nbody"},
+            {"body": None, "user": BOT},
+            {"body": f"{PR_SUMMARY_PREFIX}\n\nbody", "user": BOT},
         ]
         assert find_summary_comment(comments)["body"].startswith(PR_SUMMARY_PREFIX)
+
+    def test_ignores_non_bot_impostor(self) -> None:
+        """A non-bot comment starting with the prefix is skipped in favour of the
+        bot's — so attacker-authored region content is never read or carried forward."""
+        comments = [
+            {"body": f"{PR_SUMMARY_PREFIX}\n\n{LEAN_BEGIN}fake{LEAN_END}", "user": HUMAN},
+            {"body": f"{PR_SUMMARY_PREFIX} [real](url)\n\nbody", "user": BOT},
+        ]
+        sel = find_summary_comment(comments)
+        assert sel is not None and sel["user"]["login"] == SUMMARY_COMMENT_AUTHOR
+
+    def test_tolerates_missing_user(self) -> None:
+        """A comment with no `user` key is skipped, not fatal."""
+        assert find_summary_comment([{"body": f"{PR_SUMMARY_PREFIX}\n\nx"}]) is None