feat(ci): post per-PR comment summarising cross-reference tags

When a PR touches `Mathlib/**/*.lean` and adds `@[stacks ...]`,
`@[kerodon ...]`, or `@[wikidata ...]` attributes, this workflow posts (or
updates, or deletes) a single bot comment with one row per added tag,
showing the upstream label / description fetched from the source database,
the Mathlib declaration's first-line signature, and the author's optional
attribute comment. CI fails when any tag cannot be resolved upstream and
emits a warning (not a failure) when only transient network errors occur.

Trusted-script execution pattern (same as `PR_summary.yml`):

* The PR head is checked out into `pr-branch/` and used as DATA only — no
  code from it ever runs in this `pull_request_target` context.
* The base ref is checked out into `base/`; its
  `scripts/extract-crossref-tags.lean` and `scripts/crossref-snippet.lean`
  are the trusted versions we actually invoke, and its `lean-toolchain`
  is what `lake env lean --run` picks up.
* `mathlib-ci` is checked out via the shared `get-mathlib-ci` action;
  its `scripts/crossref_review/crossref-pr-comment.py` orchestrator
  (added in leanprover-community/mathlib-ci#39)
  drives the extract → snippet → format pipeline.
* The resulting comment file is piped through
  `scripts/pr_summary/update_PR_comment.sh` for post-once / update-in-place
  behaviour.

A startup gate exits cleanly when the base ref pre-dates the companion
Lean scripts (e.g. against an older master), so the workflow doesn't
fail spuriously.

`docs/workflows.md` gains a new entry; `scripts/README.md` points at the
mathlib-ci location for the orchestrator.

Stacked on
leanprover-community#39664
(LSP widget) and depends on the orchestrator landing in
leanprover-community/mathlib-ci#39.

Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>

Author: kim-em

.github/workflows/crossref_review.yml

@@ -0,0 +1,151 @@
+name: Cross-reference tag review
+
+# When a PR touches Mathlib/**/*.lean, run the cross-reference orchestrator
+# from `mathlib-ci` and post (or update, or delete) a single bot comment
+# summarising the `@[stacks ...]`, `@[kerodon ...]`, and `@[wikidata ...]`
+# tags it adds. Fails CI if any tag is missing upstream.
+#
+# Trusted-script execution pattern (same as `PR_summary.yml`):
+# the PR's working tree is read as DATA only. The Python orchestrator runs
+# from the `mathlib-ci` checkout, and the Lean scripts run from the
+# mathlib4 BASE checkout. Nothing from the PR checkout is ever executed in
+# this privileged context.
+on:
+  pull_request_target:
+    paths:
+      - 'Mathlib/**/*.lean'
+
+permissions:
+  contents: read
+  pull-requests: write
+
+jobs:
+  crossref-review:
+    name: post-or-update-crossref-comment
+    if: github.repository == 'leanprover-community/mathlib4'
+    runs-on: ubuntu-latest
+    env:
+      # PR description for #39666 pins this until the mathlib-ci PR (#39) merges.
+      # Once that merges, drop this and let the default in get-mathlib-ci win.
+      MATHLIB_CI_REF: 5b09178e56be069f61414284367d81166e2667d1
+
+    steps:
+      - name: Checkout PR head (data only)
+        uses: actions/checkout@de0fac2e4500dabe0009e67214ff5f5447ce83dd # v6.0.2
+        with:
+          ref: ${{ github.event.pull_request.head.sha }}
+          fetch-depth: 0
+          path: pr-branch
+
+      - name: Checkout base ref (trusted Lean scripts + toolchain)
+        uses: actions/checkout@de0fac2e4500dabe0009e67214ff5f5447ce83dd # v6.0.2
+        with:
+          ref: ${{ github.event.pull_request.base.sha }}
+          fetch-depth: 1
+          path: base
+
+      - name: Checkout local actions
+        uses: actions/checkout@de0fac2e4500dabe0009e67214ff5f5447ce83dd # v6.0.2
+        with:
+          ref: ${{ github.workflow_sha }}
+          fetch-depth: 1
+          sparse-checkout: .github/actions
+          path: workflow-actions
+
+      - name: Get mathlib-ci
+        uses: ./workflow-actions/.github/actions/get-mathlib-ci
+        with:
+          ref: ${{ env.MATHLIB_CI_REF }}
+
+      - name: Verify base has Lean scripts
+        id: gate
+        run: |
+          set -euo pipefail
+          if [ ! -f base/scripts/extract-crossref-tags.lean ] \
+             || [ ! -f base/scripts/crossref-snippet.lean ]; then
+            echo "Base ref does not have the cross-reference Lean scripts; skipping."
+            echo "skip=yes" >> "$GITHUB_OUTPUT"
+          else
+            echo "skip=no" >> "$GITHUB_OUTPUT"
+          fi
+
+      - name: Install elan
+        if: steps.gate.outputs.skip == 'no'
+        run: |
+          set -euo pipefail
+          curl https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh -sSf \
+            | sh -s -- -y --default-toolchain none
+          echo "$HOME/.elan/bin" >> "$GITHUB_PATH"
+          # First `lake env lean` invocation against `base/` will trigger
+          # download of the toolchain pinned in `base/lean-toolchain`. The
+          # scripts only import Lean core, so no Mathlib build is needed.
+
+      - name: Fetch base ref full history
+        if: steps.gate.outputs.skip == 'no'
+        run: |
+          # `--diff` mode in the extractor uses `git diff` inside `pr-branch`;
+          # we need the base ref visible there.
+          cd pr-branch
+          git fetch origin "${{ github.event.pull_request.base.ref }}" --depth=200
+
+      - name: Compose comment body
+        if: steps.gate.outputs.skip == 'no'
+        id: compose
+        run: |
+          set +e
+          python3 "${CI_SCRIPTS_DIR}/crossref_review/crossref-pr-comment.py" \
+            --pr-checkout "$(pwd)/pr-branch" \
+            --base-checkout "$(pwd)/base" \
+            --base-ref "origin/${{ github.event.pull_request.base.ref }}" \
+            --output "$(pwd)/comment.md"
+          ec=$?
+          if [ ! -f comment.md ]; then : > comment.md; fi
+          echo "exit_code=$ec" >> "$GITHUB_OUTPUT"
+          echo "---- comment.md ----"
+          cat comment.md
+          echo "---- end ----"
+
+      - name: Post or update or delete bot comment
+        if: steps.gate.outputs.skip == 'no'
+        env:
+          GH_TOKEN: ${{ secrets.GITHUB_TOKEN }}
+          GITHUB_REPOSITORY: ${{ github.repository }}
+        run: |
+          set -euo pipefail
+          PR="${{ github.event.pull_request.number }}"
+          EXIT="${{ steps.compose.outputs.exit_code }}"
+          TITLE='### Cross-reference tags added by this PR'
+          if [ "$EXIT" = "0" ] || [ ! -s comment.md ]; then
+            # No tags added → delete any prior bot comment.
+            existing=$(gh api "repos/${{ github.repository }}/issues/$PR/comments" --paginate \
+              --jq 'map(select(.body | startswith("### Cross-reference tags added by this PR"))) | first | .id // empty')
+            if [ -n "${existing:-}" ]; then
+              echo "Removing stale bot comment $existing."
+              gh api -X DELETE "repos/${{ github.repository }}/issues/comments/$existing"
+            fi
+          else
+            # Post or update via the shared helper.
+            "${CI_SCRIPTS_DIR}/pr_summary/update_PR_comment.sh" \
+              comment.md "$TITLE" "$PR"
+          fi
+
+      - name: Fail on missing tags
+        if: steps.gate.outputs.skip == 'no'
+        env:
+          EXIT: ${{ steps.compose.outputs.exit_code }}
+        run: |
+          set -euo pipefail
+          # Exit codes from crossref-pr-comment.py:
+          #   0 = no tags added (no comment posted; not a failure)
+          #   1 = tags added, all resolved
+          #   2 = some tag missing upstream  → fail
+          #   3 = transient network failure  → warn but pass
+          case "$EXIT" in
+            0|1) echo "OK." ;;
+            2)   echo "::error::One or more cross-reference tags are missing upstream."
+                 exit 1 ;;
+            3)   echo "::warning::Some cross-reference tags could not be resolved due to a network error."
+                 exit 0 ;;
+            *)   echo "::error::Unexpected exit code $EXIT from crossref-pr-comment.py"
+                 exit 1 ;;
+          esac

docs/workflows.md

@@ -50,6 +50,7 @@ Primary trigger for this section: PR/merge-queue events (`pull_request`, `pull_r
 | [`check_pr_titles.yaml`](../.github/workflows/check_pr_titles.yaml) | Check PR titles<br>[![passed/failed](https://img.shields.io/github/actions/workflow/status/leanprover-community/mathlib4/check_pr_titles.yaml?label=status)](https://github.com/leanprover-community/mathlib4/actions/workflows/check_pr_titles.yaml) | Low | `pull_request_target` | Validates PR titles against project conventions and maintains a sticky guidance comment. |
 | [`lint_and_suggest_pr.yml`](../.github/workflows/lint_and_suggest_pr.yml) | lint and suggest<br>[![passed/failed](https://img.shields.io/github/actions/workflow/status/leanprover-community/mathlib4/lint_and_suggest_pr.yml?label=status)](https://github.com/leanprover-community/mathlib4/actions/workflows/lint_and_suggest_pr.yml) | Low | `pull_request` | Runs style linting and suggests changes on pull requests. The suggested changes can be applied by calling `bot_fix_style.yaml`. |
 | [`PR_summary.yml`](../.github/workflows/PR_summary.yml) | Post PR summary comment<br>[![passed/failed](https://img.shields.io/github/actions/workflow/status/leanprover-community/mathlib4/PR_summary.yml?label=status)](https://github.com/leanprover-community/mathlib4/actions/workflows/PR_summary.yml) | Low | `pull_request_target` | On `pull_request_target`, computes PR summary data (imports/declarations/tech debt), manages related labels, and updates PR comments. |
+| [`crossref_review.yml`](../.github/workflows/crossref_review.yml) | Cross-reference tag review<br>[![passed/failed](https://img.shields.io/github/actions/workflow/status/leanprover-community/mathlib4/crossref_review.yml?label=status)](https://github.com/leanprover-community/mathlib4/actions/workflows/crossref_review.yml) | Low | `pull_request_target` | Extracts every `@[stacks]`, `@[kerodon]`, and `@[wikidata]` attribute added by the PR, fetches the upstream snippet for each, posts a once-per-PR summary comment, and fails CI if any tag is missing upstream. |
 | [`add_label_from_diff.yaml`](../.github/workflows/add_label_from_diff.yaml) | Autolabel PRs<br>[![passed/failed](https://img.shields.io/github/actions/workflow/status/leanprover-community/mathlib4/add_label_from_diff.yaml?label=status)](https://github.com/leanprover-community/mathlib4/actions/workflows/add_label_from_diff.yaml) | Low | `pull_request_target, push` | Applies an inferred topic label to newly opened PRs using `lake exe autolabel`. |
 | [`label_new_contributor.yml`](../.github/workflows/label_new_contributor.yml) | Label New Contributors<br>[![passed/failed](https://img.shields.io/github/actions/workflow/status/leanprover-community/mathlib4/label_new_contributor.yml?label=status)](https://github.com/leanprover-community/mathlib4/actions/workflows/label_new_contributor.yml) | Low | `pull_request_target` | Labels PRs from new contributors (based on the number of their PRs merged). |
 | [`zulip_emoji_closed_pr.yaml`](../.github/workflows/zulip_emoji_closed_pr.yaml) | Add "closed-pr" emoji in Zulip<br>[![passed/failed](https://img.shields.io/github/actions/workflow/status/leanprover-community/mathlib4/zulip_emoji_closed_pr.yaml?label=status)](https://github.com/leanprover-community/mathlib4/actions/workflows/zulip_emoji_closed_pr.yaml) | Low | `pull_request_target` | Updates Zulip emoji reactions for PR close/reopen events. |

scripts/README.md

@@ -255,6 +255,12 @@ to module `Foo.Bar` (no `srcDir` indirection).
   declaration it decorates. A byte-level scanner skips strings, comments,
   and modifier keywords correctly.
   `lake env lean --run scripts/extract-crossref-tags.lean --file Mathlib/Foo.lean`.
+The orchestration script driven by `.github/workflows/crossref_review.yml`
+lives in the [`mathlib-ci`](https://github.com/leanprover-community/mathlib-ci)
+repository at `scripts/crossref_review/crossref-pr-comment.py` — it is kept
+there (rather than in this repo) so the workflow can execute it from a
+trusted external checkout in the privileged `pull_request_target` context
+without running any PR-modified code.
 
 **Managing downstream repos**
 - `downstream_repos.yml` contains basic information about significant downstream repositories.