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

[adomani]

Add carry_forward + a non-patching MODE=emit so the PR-summary comment keeps a previously-shown Lean diff (relabelled) instead of reverting to pending / unavailable.

Companion: leanprover-community/mathlib4#40486 · details in the Reference / Explanation / How-to comments below.

[adomani]

Companion mathlib4 PR: leanprover-community/mathlib4#40486

[adomani]

Reference

Information-oriented. The API surface, no rationale.

carry_forward(region: str, new_heading: str) -> str | None
Returns region with its #### Declarations diff (Lean…) heading line rewritten to new_heading, iff region contains the body stamp ✅ **Lean-aware diff**; otherwise None. Strips surrounding whitespace.

Module constants

• LEAN_DIFF_STAMP = "✅ **Lean-aware diff**"
• _HEADING_RE — (?m)^#### Declarations diff \(Lean[^\n]*\)$
• PENDING_PLACEHOLDER — the (Lean -- pending) block

Modes

• emit (new) — non-patching. Prints the region content (carry-forward under NEW_HEADING, else PENDING_PLACEHOLDER) to stdout. Always exits 0. Env: REPO, NEW_HEADING, PR_NUMBER/PR_HEAD_SHA.
• warning (changed) — carry-forward under NEW_HEADING if a real diff is present, else build_warning(DEFAULT_BRANCH).
• success (unchanged).

Tests — tests/decls_diff/test_patch.py: +6 (51 total).

[adomani]

Explanation

Understanding-oriented. The design decisions.

The comment is split across two repos: mathlib4's workflows generate it, this script patches it post-build. Any fix to "what the comment shows across pushes" therefore touches both — that split is pre-existing.

A real diff is detected by its body stamp (✅ **Lean-aware diff**), not its heading. The heading is exactly what we rewrite (pending → stale → cache miss), so keying detection on it would lose the diff after the first relabel; the stamp is invariant, so a once-shown diff survives any number of relabels and only a fresh successful build replaces it.

emit is deliberately non-patching: the pre-build step rebuilds the whole comment locally and posts it in one shot, so it needs the carried-forward region as text to embed, and it must read the live comment before its own post overwrites it. A patch-in-place mode would run too late — the prior diff would already be gone.

[adomani]

How-to: verify locally

Problem-oriented. Reproduce the behaviour before merging.

1. Run the suite:

   python3 -m pytest tests/decls_diff/ -q
   

2. Exercise emit against a stubbed comment that already shows a real diff, and confirm the heading is relabelled while the body is kept:

   printf '#!/usr/bin/env bash\necho '\''[{"id":1,"body":"### PR summary\n\n<!-- DECLS_DIFF_LEAN_BEGIN -->\n#### Declarations diff (Lean)\n\n> ✅ **Lean-aware diff**\n\n* **+3** new declarations\n<!-- DECLS_DIFF_LEAN_END -->"}]'\''\n' > /tmp/gh && chmod +x /tmp/gh
   PATH=/tmp:$PATH MODE=emit NEW_HEADING='#### Declarations diff (Lean -- stale, waiting for the new build)' \
     REPO=o/r PR_NUMBER=7 PR_HEAD_SHA=x python3 scripts/pr_summary/updateDeclsDiffSection.py
   

3. Make the stub exit 1 and confirm emit still prints the pending placeholder and exits 0 (graceful degradation).

[bryangingechen]

LGTM. Feel free to merge in a coordinated way with the downstream PR.