leanprover-community · kim-em · May 21, 2026 · May 21, 2026 · May 21, 2026
diff --git a/.github/workflows/build_template.yml b/.github/workflows/build_template.yml
@@ -745,6 +745,64 @@ jobs:
       - name: clean up the import graph file
         run: rm import_graph.dot
 
+      - name: cross-reference tag review (extract added tags)
+        id: crossref
+        env:
+          # `build_fork.yml` is `pull_request_target`-triggered so the PR
+          # context is populated; `build.yml` is `push`-triggered (typically
+          # from Bors/staging), in which case `github.event.before` is the
+          # base commit. We try both. If neither is present, the step exits
+          # without producing an artifact (the workflow_run companion will
+          # see no artifact and skip).
+          PR_BASE_SHA: ${{ github.event.pull_request.base.sha }}
+          PR_BASE_REF: ${{ github.event.pull_request.base.ref }}
+          PUSH_BEFORE_SHA: ${{ github.event.before }}
+        run: |
+          set -euo pipefail
+          BASE_SHA=""
+          if [ -n "$PR_BASE_SHA" ]; then
+            BASE_SHA="$PR_BASE_SHA"
+            # post_steps checks out with default fetch-depth=1; fetch enough
+            # history to diff against base. Hard-fail on fetch errors so we
+            # don't silently turn "unknown base" into "no tags added".
+            git fetch --no-tags --depth=200 origin "$PR_BASE_REF"
+          elif [ -n "$PUSH_BEFORE_SHA" ] \
+               && [[ ! "$PUSH_BEFORE_SHA" =~ ^0{40}$ ]]; then
+            BASE_SHA="$PUSH_BEFORE_SHA"
+            git fetch --no-tags --depth=200 origin "$PUSH_BEFORE_SHA"
+          else
+            echo "No PR base or push.before available; skipping cross-reference check."
+            echo "head_sha=$(git rev-parse HEAD)" >> "$GITHUB_OUTPUT"
+            echo "skipped=yes" >> "$GITHUB_OUTPUT"
+            exit 0
+          fi
+          : > crossref-added.tsv
+          lake env lean --run scripts/crossref.lean check \
+            --diff "${BASE_SHA}..HEAD" \
+            --tsv crossref-added.tsv
+          echo "head_sha=$(git rev-parse HEAD)" >> "$GITHUB_OUTPUT"
+          echo "skipped=no" >> "$GITHUB_OUTPUT"
+
+      - name: cross-reference tag review (artifact context)
+        if: steps.crossref.outputs.skipped != 'yes' && always()
+        env:
+          PR_NUMBER: ${{ github.event.pull_request.number }}
+          HEAD_SHA: ${{ steps.crossref.outputs.head_sha }}
+        run: |
+          jq -n --arg pr "$PR_NUMBER" --arg sha "$HEAD_SHA" \
+            '{pr_number: $pr, head_sha: $sha}' > crossref-context.json
+
+      - name: upload the cross-reference artifact
+        if: steps.crossref.outputs.skipped != 'yes' && always()
+        uses: actions/upload-artifact@043fb46d1a93c77aae656e7c1c64a875d1fc6a0a # v7.0.1
+        with:
+          name: crossref-context
+          path: |
+            crossref-added.tsv
+            crossref-context.json
+          retention-days: 1
+          if-no-files-found: warn
+
       - name: check all scripts build successfully
         run: |
           lake env lean scripts/create_deprecated_modules.lean

diff --git a/.github/workflows/crossref_review.yml b/.github/workflows/crossref_review.yml
@@ -0,0 +1,158 @@
+name: Cross-reference tag review
+
+# Runs after a `build` / `build_fork` workflow finishes. The build's
+# `post_steps` job has already produced the `crossref-context` artifact
+# (a TSV of cross-reference tags whose declarations live in files the
+# PR touched, plus a small JSON with the PR number and head SHA). This
+# workflow downloads that artifact in a privileged `workflow_run`
+# context, fetches snippets, posts/updates/deletes the bot comment,
+# and exits non-zero on any tag that's missing upstream so the
+# resulting check status can gate merges.
+#
+# Privilege model: the post_steps job runs in the PR's permission
+# scope and writes only a machine-readable TSV. The TSV is parsed by
+# the orchestrator from a trusted mathlib-ci checkout; we never blindly
+# post Markdown that originated from PR code.
+
+on:
+  workflow_run:
+    workflows:
+      - "continuous integration"
+      - "continuous integration (mathlib forks)"
+    types:
+      - completed
+
+permissions:
+  contents: read
+  pull-requests: write
+  actions: read
+
+jobs:
+  crossref-review:
+    name: post-or-update-crossref-comment
+    if: github.repository == 'leanprover-community/mathlib4'
+    runs-on: ubuntu-latest
+    env:
+      # Until mathlib-ci#39's successor lands in mathlib-ci master, pin to
+      # the branch tip containing the new TSV-driven orchestrator.
+      MATHLIB_CI_REF: 78c7a682cd63d37135ec6a772c83d728819da874
+
+    steps:
+      - name: Download crossref artifact
+        id: download
+        uses: dawidd6/action-download-artifact@bf251b5aa9c2f7eeb574a96ee720e24f801b7c11 # v6
+        with:
+          name: crossref-context
+          run_id: ${{ github.event.workflow_run.id }}
+          path: artifact
+          if_no_artifact_found: warn
+
+      - name: Resolve PR number
+        id: pr
+        env:
+          HEAD_BRANCH: ${{ github.event.workflow_run.head_branch }}
+          HEAD_REPO: ${{ github.event.workflow_run.head_repository.full_name }}
+          HEAD_SHA: ${{ github.event.workflow_run.head_sha }}
+          GH_TOKEN: ${{ secrets.GITHUB_TOKEN }}
+        run: |
+          set -euo pipefail
+          PR=""
+          # Preferred: the JSON embedded by post_steps.
+          if [ -f artifact/crossref-context.json ]; then
+            PR=$(jq -r '.pr_number // empty' artifact/crossref-context.json)
+            ART_SHA=$(jq -r '.head_sha // empty' artifact/crossref-context.json)
+            if [ -n "$ART_SHA" ] && [ "$ART_SHA" != "$HEAD_SHA" ]; then
+              echo "::warning::Artifact head_sha ($ART_SHA) differs from workflow_run head_sha ($HEAD_SHA)."
+            fi
+          fi
+          # Fallback: workflow_run.pull_requests[0].number (often unreliable).
+          if [ -z "$PR" ]; then
+            PR=$(jq -r '.workflow_run.pull_requests[0].number // empty' \
+              "$GITHUB_EVENT_PATH")
+          fi
+          # Last-resort fallback: gh pr list with head sha matching.
+          if [ -z "$PR" ] && [ -n "$HEAD_REPO" ] && [ -n "$HEAD_BRANCH" ]; then
+            PR=$(gh pr list --repo "${{ github.repository }}" \
+              --head "${HEAD_REPO%%/*}:${HEAD_BRANCH}" \
+              --state open --json number,headRefOid \
+              --jq "map(select(.headRefOid == \"$HEAD_SHA\")) | first | .number // empty")
+          fi
+          echo "number=$PR" >> "$GITHUB_OUTPUT"
+          if [ -z "$PR" ]; then
+            echo "Could not resolve PR number. Skipping."
+          else
+            echo "Resolved PR number: $PR"
+          fi
+
+      - name: Checkout workflow actions
+        if: steps.pr.outputs.number != ''
+        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
+        if: steps.pr.outputs.number != ''
+        uses: ./workflow-actions/.github/actions/get-mathlib-ci
+        with:
+          ref: ${{ env.MATHLIB_CI_REF }}
+
+      - name: Compose comment body
+        if: steps.pr.outputs.number != ''
+        id: compose
+        run: |
+          set +e
+          python3 "${CI_SCRIPTS_DIR}/crossref_review/crossref-pr-comment.py" \
+            --tsv "$(pwd)/artifact/crossref-added.tsv" \
+            --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 / update / delete bot comment
+        if: steps.pr.outputs.number != ''
+        env:
+          GH_TOKEN: ${{ secrets.GITHUB_TOKEN }}
+          GITHUB_REPOSITORY: ${{ github.repository }}
+        run: |
+          set -euo pipefail
+          PR="${{ steps.pr.outputs.number }}"
+          EXIT="${{ steps.compose.outputs.exit_code }}"
+          TITLE='### Cross-reference tags added by this PR'
+          if [ "$EXIT" = "0" ] || [ ! -s comment.md ]; then
+            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
+            "${CI_SCRIPTS_DIR}/pr_summary/update_PR_comment.sh" \
+              comment.md "$TITLE" "$PR"
+          fi
+
+      - name: Fail on missing tags
+        if: steps.pr.outputs.number != ''
+        env:
+          EXIT: ${{ steps.compose.outputs.exit_code }}
+        run: |
+          set -euo pipefail
+          # Exit codes from crossref-pr-comment.py:
+          #   0 = no tags reported (no comment posted; not a failure)
+          #   1 = tags reported, all resolved
+          #   2 = some tag missing upstream  → fail this check
+          #   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
diff --git a/Mathlib.lean b/Mathlib.lean
@@ -7124,6 +7124,7 @@ public import Mathlib.Tactic.Contrapose
 public import Mathlib.Tactic.Conv
 public import Mathlib.Tactic.Convert
 public import Mathlib.Tactic.Core
+public import Mathlib.Tactic.CrossRef.Fetch
 public import Mathlib.Tactic.CrossRefAttribute
 public import Mathlib.Tactic.DSimpPercent
 public import Mathlib.Tactic.DeclarationNames
@@ -7378,6 +7379,7 @@ public import Mathlib.Tactic.Widget.Calc
 public import Mathlib.Tactic.Widget.CommDiag
 public import Mathlib.Tactic.Widget.CongrM
 public import Mathlib.Tactic.Widget.Conv
+public import Mathlib.Tactic.Widget.CrossRefHover
 public import Mathlib.Tactic.Widget.GCongr
 public import Mathlib.Tactic.Widget.InteractiveUnfold
 public import Mathlib.Tactic.Widget.LibraryRewrite

diff --git a/Mathlib/Tactic.lean b/Mathlib/Tactic.lean
@@ -74,6 +74,7 @@ public import Mathlib.Tactic.Contrapose
 public import Mathlib.Tactic.Conv
 public import Mathlib.Tactic.Convert
 public import Mathlib.Tactic.Core
+public import Mathlib.Tactic.CrossRef.Fetch
 public import Mathlib.Tactic.CrossRefAttribute
 public import Mathlib.Tactic.DSimpPercent
 public import Mathlib.Tactic.DeclarationNames
@@ -328,6 +329,7 @@ public import Mathlib.Tactic.Widget.Calc
 public import Mathlib.Tactic.Widget.CommDiag
 public import Mathlib.Tactic.Widget.CongrM
 public import Mathlib.Tactic.Widget.Conv
+public import Mathlib.Tactic.Widget.CrossRefHover
 public import Mathlib.Tactic.Widget.GCongr
 public import Mathlib.Tactic.Widget.InteractiveUnfold
 public import Mathlib.Tactic.Widget.LibraryRewrite