chore(CI): keep the previous Lean declarations diff visible while a new build runs

[adomani]

Keep the previous Lean declarations diff visible (relabelled stale) while a new build runs, instead of resetting the PR-summary comment to pending on every push.

Companion: leanprover-community/mathlib-ci#56 · details in the Reference / Explanation / How-to comments below.

[github-actions]

PR summary 0d9bc04b2a

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference

---

Declarations diff (regex)

No declarations were harmed in the making of this PR! 🐙

You can run this locally as follows

## from your `mathlib4` directory:
git clone https://github.com/leanprover-community/mathlib-ci.git ../mathlib-ci

## summary with just the declaration names:
../mathlib-ci/scripts/pr_summary/declarations_diff.sh <optional_commit>

## more verbose report:
../mathlib-ci/scripts/pr_summary/declarations_diff.sh long <optional_commit>

The doc-module for scripts/pr_summary/declarations_diff.sh in the mathlib-ci repository contains some details about this script.

Declarations diff (Lean -- pending)

Computed after the build finishes.

---

No changes to strong technical debt.

No changes to weak technical debt.

Current commit 0d9bc04b2a
Reference commit f430c19489

This script lives in the mathlib-ci repository. To run it locally, from your mathlib4 directory:

git clone https://github.com/leanprover-community/mathlib-ci.git ../mathlib-ci
../mathlib-ci/scripts/reporting/technical-debt-metrics.sh pr_summary

• The relative value is the weighted sum of the differences with weight given by the inverse of the current value of the statistic.
• The absolute value is the relative value divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).

---

⚠️ Workflow documentation reminder

This PR modifies files under .github/workflows/.
Please update docs/workflows.md if the workflow inventory, triggers, or behavior changed.

Modified workflow files:

• .github/workflows/PR_summary.yml
• .github/workflows/decls-diff.yml

[adomani]

Reference

Information-oriented. What changed, no rationale.

Files

• .github/workflows/PR_summary.yml (pre-build, pull_request_target)
• .github/workflows/decls-diff.yml (post-build, workflow_run)

PR_summary.yml — the hard-coded (Lean -- pending) placeholder is replaced by a call to mathlib-ci's updateDeclsDiffSection.py:

• env: MODE=emit, NEW_HEADING='#### Declarations diff (Lean -- stale, waiting for the new build)', REPO, PR_NUMBER, PR_HEAD_SHA
• stdout is captured into the DECLS_DIFF_LEAN_BEGIN/END region
• || printf '#### Declarations diff (Lean -- pending)\n\n_Computed after the build finishes._' is the fallback

decls-diff.yml — the warning (cache-miss) step gains:

• NEW_HEADING='#### Declarations diff (Lean -- cache miss, showing previous diff)'

Heading states: (Lean) · (Lean -- pending) · (Lean -- stale, waiting for the new build) · (Lean -- cache miss, showing previous diff) · (Lean -- unavailable).

The post-build success path is unchanged.

[adomani]

Explanation

Understanding-oriented. Why, not how.

The PR-summary comment holds a Lean-aware declarations-diff region that only the post-build workflow can fill — it needs the build's decls.txt/imports.json artifacts, which do not exist pre-build. The pre-build workflow runs on every push and rewrites the whole comment, so before this change it overwrote any real diff with the pending placeholder, and the good diff disappeared until the next build finished.

Rather than recompute (impossible pre-build), the pre-build step now reuses what is already on the comment: if a real diff is present it is carried forward verbatim with only its heading relabelled stale. So the content a reader sees is always the last truly-computed diff, never a blank — only a newer successful build replaces it.

The fallback exists because the carry-forward reads the live comment via gh; if that call ever fails the step must still post a sensible placeholder rather than break the summary. The cache-miss heading is separate from stale so the two situations remain distinguishable to a reader.

[adomani]

How-to: merge this safely

Problem-oriented. The steps to land it without breaking the summary comment.

mathlib4 CI runs the script at the pinned get-mathlib-ci ref, not mathlib-ci master. MODE=emit only exists once that ref includes leanprover-community/mathlib-ci#56. So:

1. Merge mathlib-ci#56 first.
2. Let the dependency bot bump the pinned get-mathlib-ci ref to a commit that contains MODE=emit (or bump it manually in .github/actions/get-mathlib-ci/action.yml).
3. Merge this PR.

If this merges while the pinned ref still points at the old script, MODE=emit is unrecognised there: it exits 0 after printing a diagnostic to stdout, and that line is captured into the comment region. The || printf fallback does not save you (it only triggers on non-zero exit). Hence the ordering above.

[SnirBroshi]

Which of the two NEW_HEADING variables you've defined is what's shown to the user? The "cache miss" version or the "stale" version?

[adomani]

The intent is that as soon as one Lean-aware diff has been shown, there will always be one visible in the message. What changes is the header.

• When the Lean-aware diff is correct, you will see (Lean).
• When the Lean-aware is stale and CI is running, you will see (Lean -- pending).
• When the Lean-aware is stale and there was a cache miss, you will see (Lean -- cache miss).

Does this answer your question?

[SnirBroshi]

Does this answer your question?

Almost, but the code does not contain the string (Lean -- cache miss) anywhere.
My question was between the NEW_HEADING in decls-diff.yml and the NEW_HEADING in PR_summary.yml.

If the answer is that the former will be shown, then:

• Why is the latter needed? Can you delete it?
• I think "stale" is a better user-facing term than "cache miss" which is a computer-science term, and I also think "waiting for the new build" sounds better than "showing previous diff" (or even better: include both)

[adomani]

I spoke too quickly! Here are the actual options:

• (Lean) a fresh, post-build diff
• (Lean -- pending) first run on the PR, no diff computed yet
• (Lean -- stale, waiting for the new build) after a push — previous diff kept while the new build runs (set in PR_summary.yml)
• (Lean -- cache miss, showing previous diff) after a build that cache-missed — previous diff kept (set in decls-diff.yml)
• (Lean -- unavailable) cache miss when there's no previous diff to fall back on

Having said that, if you think that using (Lean -- stale, cache miss on the last build) in the cache miss case is clearer, I am happy to make the change!

[SnirBroshi]

I think we should avoid the term "cache-miss" entirely but I might be misunderstanding what it means here.
If the distinction is "build in-progress" vs "build failed" then we should say those instead.

[adomani]

The name originally came from the fact that not every commit to master comes with a cache: (as far as I understand) when bors merges a batch, it creates a commit for each PR in the batch, but only runs CI on the combination of the commits. The "intermediate" commits do not have a cache. When I was writing the first version of the script, I was worried of a situation where the merge-base was a "cache-less" commit and hence referred to the situation as "cache miss".

However, it turns out that, unless you explicitly try to aim for a cache-less commit, the merge-base is a cache-full commit! At that point, the concern became that the artifact containing the names of the declarations on master was present. By continuity, this case kept the name of "cache miss", even though, at this point, maybe "missing master declaration data" would have been more appropriate.

So, if you prefer to use a different name for this situation, then I am happy to take suggestions!

[SnirBroshi]

How about "please merge master"?

[adomani]

Ok, let's go with (Lean -- stale; merge master and push to refresh).

[bryangingechen]

Thanks!
bors d+

[mathlib-bors]

✌️ adomani can now approve this pull request until 2026-06-25 01:49 UTC (in 2 weeks). To approve and merge, reply with bors r+. More detailed instructions are available here.

⚠️ This delegation only covers changes within Archive/**, Counterexamples/**, docs/**, DownstreamTest/**, Mathlib/**, MathlibTest/**, widget/**, Archive.lean, Counterexamples.lean, docs.lean, Mathlib.lean; an author commit touching anything else will revoke it. Bors also revokes it if a later push changes too many files for it to check the full list — even if it stays within scope.

[mathlib-bors]

⏳ @adomani, your delegation on this PR expires in less than a week (approximately 6 days, 23 hours, at 2026-06-25 01:49 UTC).

[mathlib-bors]

⏳ @adomani, your delegation on this PR expires in less than 24 hours (approximately 23 hours, 59 minutes, at 2026-06-25 01:49 UTC).

[mathlib-bors]

⌛ Delegation for @adomani on this PR has expired (at 2026-06-25 01:49 UTC). Reply with bors d+ or bors d=adomani with a for= argument to re-delegate.