decls-diff.yml

# Post-build workflow that patches the `### PR summary` comment with a
# Lean-aware declarations diff after each successful PR build. Consumes the
# `import-graph` artifact uploaded by `build_template.yml` on both sides
# (PR head + master merge-base), computes the diff via mathlib-ci's
# `decls-diff` action, and replaces the `#### Declarations diff (Lean ...)`
# region of the comment (the regex block is left untouched). On a cache miss
# it marks that region unavailable instead.

name: Declarations diff (post-build)

on:
  workflow_run:
    # Match the build workflows by their `name:` — `build.yml` (non-fork PRs,
    # push-triggered) and `build_fork.yml` (fork PRs, pull_request_target).
    workflows: ["continuous integration", "continuous integration (mathlib forks)"]
    types: [completed]

# Per upstream PR (repo + branch), keep only the latest post-build run so rapid
# pushes don't race to patch the comment with a stale diff.
concurrency:
  group: ${{ github.workflow }}-${{ github.event.workflow_run.head_repository.full_name }}-${{ github.event.workflow_run.head_branch }}
  cancel-in-progress: true

permissions:
  contents: read
  actions: read           # for cross-workflow artifact downloads
  pull-requests: write    # for PATCHing the `### PR summary` comment

jobs:
  diff:
    # The build never runs on a `pull_request` event: non-fork PRs build via
    # `build.yml` on `push` (head_branch = the PR branch), fork PRs via
    # `build_fork.yml` on `pull_request_target`. Accept both, and for `push`
    # exclude master and the non-PR maintenance branches.
    if: >-
      github.repository == 'leanprover-community/mathlib4'
      && github.event.workflow_run.conclusion == 'success'
      && (
        github.event.workflow_run.event == 'pull_request_target'
        || (
          github.event.workflow_run.event == 'push'
          && github.event.workflow_run.head_branch != 'master'
          && github.event.workflow_run.head_branch != 'nightly-testing'
        )
      )
    runs-on: ubuntu-latest
    steps:
      - name: Resolve Build run + SHA
        id: meta
        run: |
          set -euo pipefail
          RUN_ID="${{ github.event.workflow_run.id }}"
          NEW_SHA="${{ github.event.workflow_run.head_sha }}"
          {
            echo "run-id=$RUN_ID"
            echo "new-sha=$NEW_SHA"
          } | tee -a "$GITHUB_OUTPUT"

      - name: Checkout new commit
        uses: actions/checkout@3d3c42e5aac5ba805825da76410c181273ba90b1 # v7.0.1
        with:
          ref: ${{ steps.meta.outputs.new-sha }}
          fetch-depth: 0
          # `new-sha` is fork PR code already built by build_fork.yml; allow the
          # fork checkout under this workflow_run.
          allow-unsafe-pr-checkout: true
          persist-credentials: false

      - name: Resolve merge-base against master
        id: resolve
        env:
          NEW_SHA: ${{ steps.meta.outputs.new-sha }}
        run: |
          set -euo pipefail
          git fetch --quiet origin master
          MB="$(git merge-base "$NEW_SHA" origin/master)"
          echo "merge-base=$MB" | tee -a "$GITHUB_OUTPUT"

      - name: Download new-side artifact
        uses: actions/download-artifact@3e5f45b2cfb9172054b4087a40e8e0b5a5461e7c # v8.0.1
        with:
          name: import-graph
          path: ./new-artifact
          run-id: ${{ steps.meta.outputs.run-id }}
          github-token: ${{ secrets.GITHUB_TOKEN }}

      - name: Resolve PR number
        id: pr
        env:
          GH_TOKEN: ${{ secrets.GITHUB_TOKEN }}
          REPO: ${{ github.repository }}
          NEW_SHA: ${{ steps.meta.outputs.new-sha }}
        run: |
          set -euo pipefail
          # The build records the PR number in the artifact — reliable for fork
          # PRs, where the commit-SHA search API lags or misses. Fall back to the
          # commit's associated PRs for same-repo pushes (commit is on this repo);
          # these include every open PR whose branch contains the commit, so take
          # the one whose head it is.
          PR_NUMBER="$(tr -dc '0-9' < ./new-artifact/pr_number.txt 2>/dev/null || true)"
          if [ -z "$PR_NUMBER" ]; then
            PR_NUMBER="$(gh api "repos/$REPO/commits/$NEW_SHA/pulls" \
                          --jq "[.[] | select(.head.sha == \"$NEW_SHA\")] | .[0].number // empty")"
          fi
          # For fork PRs the artifact was produced by PR code, so the number is
          # untrusted: only accept a PR whose current head is the commit we built.
          if [ -n "$PR_NUMBER" ]; then
            if ! HEAD_SHA="$(gh api "repos/$REPO/pulls/$PR_NUMBER" --jq '.head.sha')"; then
              echo "::warning::Could not read PR #$PR_NUMBER to check its head; not patching."
              PR_NUMBER=""
            elif [ "$HEAD_SHA" != "$NEW_SHA" ]; then
              echo "::notice::PR #$PR_NUMBER head is $HEAD_SHA, not $NEW_SHA; not patching."
              PR_NUMBER=""
            fi
          fi
          echo "pr-number=$PR_NUMBER" | tee -a "$GITHUB_OUTPUT"

      - name: Find master Build for the merge-base
        id: master-run
        # Without a verified PR number there is nothing to patch. Skipping this
        # step leaves `found` unset, so the diff steps below are skipped too.
        if: steps.pr.outputs.pr-number != ''
        env:
          GH_TOKEN: ${{ secrets.GITHUB_TOKEN }}
          REPO: ${{ github.repository }}
          MB: ${{ steps.resolve.outputs.merge-base }}
        run: |
          set -euo pipefail
          RUN="$(gh api "repos/$REPO/actions/runs?head_sha=$MB&event=push&status=success&branch=master" \
                  --jq '[.workflow_runs[] | select(.name=="continuous integration")] | .[0].id // ""')"
          # A successful run is not enough: it must also carry the `import-graph` artifact.
          HAS_ARTIFACT=""
          if [ -n "$RUN" ]; then
            HAS_ARTIFACT="$(gh api "repos/$REPO/actions/runs/$RUN/artifacts" \
                    --jq '[.artifacts[] | select(.name=="import-graph")] | length')"
          fi
          if [ -n "$RUN" ] && [ "${HAS_ARTIFACT:-0}" -gt 0 ]; then
            {
              echo "found=true"
              echo "run-id=$RUN"
            } | tee -a "$GITHUB_OUTPUT"
          else
            echo "found=false" | tee -a "$GITHUB_OUTPUT"
            echo "No usable master Build for merge-base $MB (no run, or run lacks the import-graph artifact)."
          fi

      - name: Download master-side artifact
        if: steps.master-run.outputs.found == 'true'
        uses: actions/download-artifact@3e5f45b2cfb9172054b4087a40e8e0b5a5461e7c # v8.0.1
        with:
          name: import-graph
          path: ./ref-artifact
          run-id: ${{ steps.master-run.outputs.run-id }}
          github-token: ${{ secrets.GITHUB_TOKEN }}

      # Tooling is checked out whenever there is a PR to patch, not only when the
      # diff is computed: the patcher (from CI_SCRIPTS_DIR) is needed on the
      # cache-miss path too, to post the warning notice.
      - name: Checkout local actions
        if: steps.pr.outputs.pr-number != ''
        uses: actions/checkout@3d3c42e5aac5ba805825da76410c181273ba90b1 # v7.0.1
        with:
          ref: ${{ github.workflow_sha }}
          fetch-depth: 1
          sparse-checkout: .github/actions
          path: workflow-actions
          persist-credentials: false # no later step needs git credentials

      - name: Get mathlib-ci
        if: steps.pr.outputs.pr-number != ''
        uses: ./workflow-actions/.github/actions/get-mathlib-ci

      - name: Compute Lean-aware declarations diff
        if: steps.master-run.outputs.found == 'true'
        id: diff
        uses: ./ci-tools/.github/actions/decls-diff
        with:
          reference-decls-file:   ${{ github.workspace }}/ref-artifact/decls.txt
          reference-imports-file: ${{ github.workspace }}/ref-artifact/imports.json
          new-decls-file:         ${{ github.workspace }}/new-artifact/decls.txt
          new-imports-file:       ${{ github.workspace }}/new-artifact/imports.json
          new-sha:                ${{ steps.meta.outputs.new-sha }}
          with-heading:           'true'

      # Keep both patcher steps gated on a non-empty PR number: given an empty
      # PR_NUMBER, the patcher looks one up from the commit SHA, unverified.
      - name: Patch PR summary comment (success)
        if: steps.master-run.outputs.found == 'true' && steps.pr.outputs.pr-number != ''
        env:
          GH_TOKEN:      ${{ secrets.GITHUB_TOKEN }}
          REPO:          ${{ github.repository }}
          PR_HEAD_SHA:   ${{ steps.meta.outputs.new-sha }}
          PR_NUMBER:     ${{ steps.pr.outputs.pr-number }}
          MODE:          success
          OVERRIDE_FILE: ${{ steps.diff.outputs.decls-override-file }}
        run: python3 "$CI_SCRIPTS_DIR/pr_summary/updateDeclsDiffSection.py"

      - name: Note cache miss
        if: steps.master-run.outputs.found != 'true' && steps.pr.outputs.pr-number != ''
        env:
          GH_TOKEN:       ${{ secrets.GITHUB_TOKEN }}
          REPO:           ${{ github.repository }}
          PR_HEAD_SHA:    ${{ steps.meta.outputs.new-sha }}
          PR_NUMBER:      ${{ steps.pr.outputs.pr-number }}
          MODE:           warning
          DEFAULT_BRANCH: master
          # If a real diff is already shown, keep it (relabelled) rather than
          # blanking it to "unavailable" and give an actionable remedy.
          NEW_HEADING:    '#### Declarations diff (Lean -- stale; merge master and push to refresh)'
        run: |
          # Record the cache miss in the step summary first, so a later patcher
          # error (e.g. a transient GitHub failure) still leaves this run-local
          # note; then mark the comment's Lean region unavailable.
          {
            echo "## Declarations diff"
            echo
            echo "⚠️ The Mathlib cache for this PR's merge-base \`${{ steps.resolve.outputs.merge-base }}\` isn't on the server (typically because the merge-base is a bors-batch intermediate that CI never built). Merge \`master\` into this PR and push to retrigger the build."
          } >> "$GITHUB_STEP_SUMMARY"
          python3 "$CI_SCRIPTS_DIR/pr_summary/updateDeclsDiffSection.py"