feat(ci): cross-reference tag review via post-build lint + workflow_run

[kim-em]

Cross-reference tag review for PRs adding @[stacks ...], @[kerodon ...], or @[wikidata ...] attributes — implemented as a post-build lint step plus a workflow_run-triggered companion that posts the bot comment.

Why this shape. The previous iteration of this PR ran an independent pull_request_target workflow that text-parsed PR source files. That was a workaround for not having a built Mathlib environment available in CI. With a post-build lint step we do have the elaborated environment — so we read Mathlib.CrossRef.tagExt directly via importModules (loadExts := true) and cut ~250 LOC of bespoke byte-level scanner.

The three pieces:

• scripts/crossref.lean — the extract subcommand is gone. New check --diff <range> --tsv <path> subcommand walks tagExt, looks up each tagged declaration's source module via env.getModuleFor?, filters by git diff --name-only of the PR range, and writes a machine-readable TSV. No Markdown, no network, no snippet fetching — that's the privileged workflow's job. Note: withImportModules passes loadExts := false and would leave tagExt empty for imported modules; we use importModules (loadExts := true) instead.

• .github/workflows/build_template.yml — three new steps in post_steps, after the existing import-graph upload:

  1. lake env lean --run scripts/crossref.lean check --diff "${BASE_SHA}..HEAD" --tsv crossref-added.tsv
  2. Write crossref-context.json carrying the PR number and head SHA (so the workflow_run job doesn't have to rely on the unreliable workflow_run.pull_requests[0].number).
  3. Upload both as a single crossref-context artifact.

• .github/workflows/crossref_review.yml — rewritten. Trigger flips from pull_request_target to workflow_run on the build workflows. Downloads the artifact, resolves the PR number through a three-stage fallback (artifact JSON → workflow_run payload → gh pr list head SHA match), calls the mathlib-ci orchestrator (which now consumes the TSV and fetches snippets in Python directly with parallel ThreadPoolExecutor for Stacks/Kerodon), and posts via update_PR_comment.sh. Fails the check on any missing tag.

Privilege model. The lint step runs with the PR's permissions and produces only a machine-readable TSV. The workflow_run job runs in the base ref's permission scope (with pull-requests: write), never executes anything from the artifact, fetches snippets server-side from three fixed upstream APIs, and builds the Markdown comment in trusted code.

• depends on: feat(CrossRefAttribute): info-view widget for cross-reference tags #39664
• depends on: refactor(crossref_review): consume TSV from mathlib4's post-build lint mathlib-ci#39 (rewrites the orchestrator to consume the TSV)

🤖 Prepared with Claude Code

[github-actions]

PR summary 292d3968f8

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference
Mathlib.Tactic	2
Mathlib.Tactic.CrossRef.Fetch (new file)	54

---

Declarations diff

+ CheckArgs
+ CrossRefHoverPanel
+ CrossRefHoverPanel.rpc
+ CrossRefHoverProps
+ Database.fetch
+ Database.gerbyBase?
+ Database.ofName?
+ Database.ofName?_name
+ Database.ofString?
+ Database.ofString?_name
+ Result
+ Result.emit
+ SnippetOutcome
+ WikidataParse
+ attachCrossRefWidget
+ cacheFile?
+ cacheLoad
+ cacheStore
+ checkUsage
+ fetchGerbyAll
+ fetchSnippet
+ gerbyBase?
+ gitChangedFiles
+ moduleToFilePath
+ parseCheckArgs
+ parseWikidataResponse
+ renderOutcome
+ snippetMain
+ snippetUsage
+ usage
+ wikidataBatchSize
+ wikidataResultOf
++ Database.name
++ afterFirst?
++ fetchGerby
++ fetchUrl
++ fetchWikidata
++ flattenWhitespace
++ jsonStrPath?
++ parseGerbyTitle
++ stripHtml
++ takeUntilChar
++ userAgent
+-+ Database

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.

---

No changes to strong technical debt.

No changes to weak technical debt.

---

⚠️ 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/build_template.yml
• .github/workflows/crossref_review.yml

---

⚠️ Scripts folder reminder

This PR adds files under scripts/.
Please consider whether each added script belongs in this repository or in leanprover-community/mathlib-ci.

A script belongs in mathlib-ci if it is a CI automation script that interacts with GitHub (e.g. managing labels, posting comments, triggering bots), runs from a trusted external checkout in CI, or requires access to secrets.

A script belongs in this repository (scripts/) if it is a developer or maintainer tool to be run locally, a code maintenance or analysis utility, a style linting tool, or a data file used by the library's own linters.

See the mathlib-ci README for more details.

Added scripts files:

• scripts/crossref.lean

[mathlib-dependent-issues]

This PR/issue depends on:

• feat(CrossRefAttribute): info-view widget for cross-reference tags #39664
• refactor(crossref_review): consume TSV from mathlib4's post-build lint mathlib-ci#39
  By Dependent Issues (🤖). Happy coding!

[kim-em]

Here's what the bot's comment renders as, generated by feeding the orchestrator a synthetic file with one valid + one bogus tag from each database. (No quoting trick — this is the literal contents of comment.md from a real run, dropped into a GitHub comment so you can see how the table actually displays.)

---

Cross-reference tags added by this PR

Wikidata

Tag	Declaration	Title	Snippet	Author comment
Q11518	theorem pythagoras : True	Pythagorean theorem	relation in Euclidean geometry among the three sides of a right triangle	named after Pythagoras
QFAKE99999	theorem bad : True	⚠ NOT FOUND		intentionally bogus

Stacks

Tag	Declaration	Title	Snippet	Author comment
09FS	theorem cohen_first (n : ℕ) [NeZero n] : True	Example 9.5.2	Example 9.5.2. The characteristic of $\mathbf{F}_ p$ is $p$, and that of $\mathbf{Q}$ is $0$.	First part. We don't require p to be a prime in mathlib.
ZZZZ	theorem worse : True	⚠ NOT FOUND		also bogus

Kerodon

Tag	Declaration	Title	Snippet	Author comment
0009	theorem first_notation : True	Notation 1.1.0.1	Notation 1.1.0.1. For every nonnegative integer $n$, we let $[n]$ denote the linearly ordered set ${ 0 < 1 < 2 < \cdots < n-1 < n } $.

⚠ One or more tags above could not be found upstream. Please verify the tag identifier or remove the attribute.

[kim-em]

Closing in favour of #39877, which uses the existing privilege-escalation-bridge pattern (see olean_report.yaml + olean_report_wf_run.yaml) and delegates snippet-fetching / comment-rendering to https://github.com/leanprover-community/external-tags.

This drops the ~250 LOC of bespoke artifact / PR-resolution machinery and the entire extract / check subcommand from scripts/crossref.lean.