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

Stack on top of the dump_crossref_tags.lean PR. Adds two pieces:

* .github/workflows/build_template.yml: three new steps in `post_steps`,
  after the import-graph upload. Run scripts/dump_crossref_tags.lean to
  produce crossref-tags.tsv. For pull_request_target builds, build a
  bridge payload (pr_number, head_sha) and emit it via
  leanprover-community/privilege-escalation-bridge/emit using artifact
  name `crossref-tags-bridge`. Non-PR builds skip the emit.

* .github/workflows/crossref_review.yml: workflow_run listener on
  the two `continuous integration` workflows. Consumes the bridge
  artifact via privilege-escalation-bridge/consume, checks out
  leanprover-community/mathlib-ci, and invokes its
  scripts/crossref_review/post-comment.sh orchestrator. The orchestrator
  clones leanprover-community/external-tags at a pinned SHA and uses it
  to fetch snippets and render the PR comment.

Replaces #39666. The original PR rolled its own artifact upload + PR
number resolution fallback chain (~158 LOC) and included the snippet
fetcher in scripts/crossref.lean (~760 LOC). This version delegates to
the existing privilege-escalation-bridge infrastructure (same pattern
as olean_report.yaml + olean_report_wf_run.yaml) and to external-tags,
cutting the mathlib4 surface to ~97 LOC.

Trust model: the privileged workflow_run job runs only code from
mathlib-ci@<pinned SHA> (which runs only code from external-tags at a
pinned SHA). Nothing from the build artifact is interpreted as code;
the TSV is parsed as untrusted data with user-controllable fields
escaped before interpolation into the comment.

Depends on #39876.

Co-Authored-By: Claude Opus 4.7 <noreply@anthropic.com>

Author: kim-em

.github/workflows/build_template.yml

@@ -745,6 +745,41 @@ jobs:
       - name: clean up the import graph file
         run: rm import_graph.dot
 
+      - name: dump cross-reference tags to TSV
+        # Walks Mathlib.CrossRef.tagExt and writes one TSV row per @[stacks ...] /
+        # @[kerodon ...] / @[wikidata ...] tag for the privileged workflow_run
+        # job (crossref_review.yml) to consume. The script has no network access
+        # and enforces a 2 MB output cap.
+        run: lake env lean --run scripts/dump_crossref_tags.lean crossref-tags.tsv
+
+      - name: prepare crossref bridge outputs
+        # We only emit the crossref bridge artifact when this build is for a PR
+        # (the `crossref_review.yml` workflow_run job has nothing to post otherwise).
+        id: crossref_outputs
+        env:
+          EVENT_NAME: ${{ github.event_name }}
+          HEAD_SHA: ${{ inputs.pr_branch_ref }}
+          PR_NUMBER: ${{ github.event.pull_request.number }}
+        run: |
+          if [ "$EVENT_NAME" = "pull_request_target" ] && [ -n "$PR_NUMBER" ]; then
+            jq -n --arg n "$PR_NUMBER" --arg s "$HEAD_SHA" \
+              '{ pr_number: $n, head_sha: $s }' > crossref-bridge-outputs.json
+            echo "emit=true" >> "$GITHUB_OUTPUT"
+          else
+            echo "emit=false" >> "$GITHUB_OUTPUT"
+          fi
+
+      - name: emit crossref bridge artifact
+        if: steps.crossref_outputs.outputs.emit == 'true'
+        uses: leanprover-community/privilege-escalation-bridge/emit@f5dfe313a79647c07315b451b2dc2a81a161a50d # v1.2.0
+        with:
+          artifact: crossref-tags-bridge
+          outputs_file: crossref-bridge-outputs.json
+          include_event: minimal
+          files: |
+            crossref-tags.tsv
+          retention_days: 5
+
       - name: check all scripts build successfully
         run: |
           lake env lean scripts/create_deprecated_modules.lean

.github/workflows/crossref_review.yml

@@ -0,0 +1,62 @@
+# Cross-reference tag review (workflow_run)
+#
+# Privileged companion to the `dump cross-reference tags to TSV` step in
+# `build_template.yml`. Downloads the bridge artifact emitted by the build,
+# hands off to mathlib-ci's orchestrator, which in turn invokes the
+# pinned `leanprover-community/external-tags` tool to fetch snippets and
+# produce the PR comment body, then posts/updates the comment.
+#
+# The privileged job runs with `pull-requests: write`, but it executes only
+# code from mathlib-ci (which executes only code from external-tags at a
+# pinned SHA). Nothing from the build artifact is interpreted as code; the
+# TSV is parsed as untrusted data.
+name: cross-reference review (workflow_run)
+
+on:
+  workflow_run:
+    workflows:
+      - continuous integration
+      - continuous integration (mathlib forks)
+    types:
+      - completed
+
+permissions:
+  actions: read
+  contents: read
+  pull-requests: write
+
+jobs:
+  review:
+    name: Post cross-reference review comment
+    runs-on: ubuntu-latest
+    if: ${{ github.repository == 'leanprover-community/mathlib4' && github.event.workflow_run.conclusion == 'success' }}
+    steps:
+      - name: Consume bridge artifact
+        id: bridge
+        uses: leanprover-community/privilege-escalation-bridge/consume@f5dfe313a79647c07315b451b2dc2a81a161a50d # v1.2.0
+        with:
+          token: ${{ github.token }}
+          artifact: crossref-tags-bridge
+          # Pushes (non-PR builds) intentionally skip the emit step, so a
+          # missing artifact is the common case for non-PR runs.
+          fail_on_missing: false
+          extract: |
+            pr_number=outputs.pr_number
+            head_sha=outputs.head_sha
+
+      - name: Checkout mathlib-ci
+        if: steps.bridge.outputs.pr_number != ''
+        uses: actions/checkout@de0fac2e4500dabe0009e67214ff5f5447ce83dd # v6.0.2
+        with:
+          repository: leanprover-community/mathlib-ci
+          ref: master
+          path: mathlib-ci
+
+      - name: Run cross-reference review
+        if: steps.bridge.outputs.pr_number != ''
+        env:
+          GH_TOKEN: ${{ github.token }}
+          PR_NUMBER: ${{ steps.bridge.outputs.pr_number }}
+          HEAD_SHA: ${{ steps.bridge.outputs.head_sha }}
+          TSV_PATH: ${{ github.workspace }}/.bridge/crossref-tags.tsv
+        run: bash mathlib-ci/scripts/crossref_review/post-comment.sh