Merge branch 'master' into partial-type

Author: NoneMore

.github/workflows/build_template.yml

@@ -816,17 +816,7 @@ jobs:
     needs: [style_lint, build, post_steps]
     runs-on: ubuntu-latest
     steps:
-      - name: Generate auto merge app token
-        id: auto-merge-app-token
-        uses: leanprover-community/mathlib-ci/.github/actions/azure-create-github-app-token@3bb576208589a435eeaeac9b144a1b7c3e948760
-        with:
-          app-id: ${{ secrets.MATHLIB_AUTO_MERGE_APP_ID }}
-          key-vault-name: ${{ vars.MATHLIB_AZ_KEY_VAULT_NAME }}
-          key-name: mathlib-auto-merge-app-pk
-          azure-client-id: ${{ vars.GH_APP_AZURE_CLIENT_ID_CI_AUTO_MERGE }}
-          azure-tenant-id: ${{ secrets.LPC_AZ_TENANT_ID }}
-
-      - id: PR_from_push
+      - id: PR
         uses: 8BitJonny/gh-get-current-pr@4056877062a1f3b624d5d4c2bedefa9cf51435c9 # 4.0.0
         # TODO: this may not work properly if the same commit is pushed to multiple branches:
         # https://github.com/8BitJonny/gh-get-current-pr/issues/8
@@ -835,16 +825,6 @@ jobs:
           # Only return if PR is still open
           filterOutClosed: true
 
-      # TODO: delete this step and rename `PR_from_push` to `PR` if the above step seems to work properly
-      # Combine the output from the previous action with the metadata supplied by GitHub itself.
-      # Note that if we fall back to github.event.pull_request data, the list of labels is generated when this workflow is triggered
-      # and not updated afterwards!
-      - id: PR
-        shell: bash
-        run: |
-          echo "number=${{ steps.PR_from_push.outputs.number || github.event.pull_request.number }}" | tee -a "$GITHUB_OUTPUT"
-          echo "pr_labels=${{ steps.PR_from_push.outputs.pr_labels || join(github.event.pull_request.labels.*.name, ',') }}" | tee -a "$GITHUB_OUTPUT"
-
       - id: remove_labels
         name: Remove "awaiting-CI"
         # we use curl rather than octokit/request-action so that the job won't fail
@@ -854,6 +834,17 @@ jobs:
             --url https://api.github.com/repos/${{ github.repository }}/issues/${{ steps.PR.outputs.number }}/labels/awaiting-CI \
             --header 'authorization: Bearer ${{ secrets.GITHUB_TOKEN }}'
 
+      - if: contains(steps.PR.outputs.pr_labels, 'auto-merge-after-CI')
+        name: Generate auto merge app token
+        id: auto-merge-app-token
+        uses: leanprover-community/mathlib-ci/.github/actions/azure-create-github-app-token@3bb576208589a435eeaeac9b144a1b7c3e948760
+        with:
+          app-id: ${{ secrets.MATHLIB_AUTO_MERGE_APP_ID }}
+          key-vault-name: ${{ vars.MATHLIB_AZ_KEY_VAULT_NAME }}
+          key-name: mathlib-auto-merge-app-pk
+          azure-client-id: ${{ vars.GH_APP_AZURE_CLIENT_ID_CI_AUTO_MERGE }}
+          azure-tenant-id: ${{ secrets.LPC_AZ_TENANT_ID }}
+
       - if: contains(steps.PR.outputs.pr_labels, 'auto-merge-after-CI')
         name: Get PR label timeline data
         # 'auto-merge-after-CI' must be within the last 100 labels added (could be increased to 250 if needed)

.github/workflows/commit_verification.yml

@@ -3,7 +3,7 @@
 #
 # - Transient commits (prefix: "transient: ") must have zero net effect
 # - Automated commits (prefix: "x: <command>") must match command output
-# - Posts a summary comment categorizing commits for reviewers
+# - Uploads a workflow artifact with verification status and a comment to be posted on the PR
 
 name: Commit Verification
 
@@ -18,7 +18,6 @@ concurrency:
 
 permissions:
   contents: read
-  pull-requests: write
 
 env:
   TRANSIENT_PREFIX: "transient: "
@@ -67,6 +66,7 @@ jobs:
           else
             echo "has_special=false" >> "$GITHUB_OUTPUT"
             echo "No transient or automated commits found"
+            echo "No transient or automated commits found; this comment should never be posted" > comment_body.md
           fi
 
       - name: Verify commits
@@ -100,26 +100,22 @@ jobs:
           # Save to file (GitHub Actions has issues with multiline outputs)
           echo "$COMMENT" > comment_body.md
 
-      - name: Find existing comment
-        if: steps.check.outputs.has_special == 'true'
-        uses: peter-evans/find-comment@b30e6a3c0ed37e7c023ccd3f1db5c6c0b0c23aad # v4
-        id: find-comment
-        with:
-          issue-number: ${{ github.event.pull_request.number }}
-          comment-author: 'github-actions[bot]'
-          body-includes: 'Commit Verification Summary'
-
-      - name: Post or update comment
-        if: steps.check.outputs.has_special == 'true'
-        uses: peter-evans/create-or-update-comment@e8674b075228eee787fea43ef493e45ece1004c9 # v4
-        with:
-          comment-id: ${{ steps.find-comment.outputs.comment-id }}
-          issue-number: ${{ github.event.pull_request.number }}
-          body-path: comment_body.md
-          edit-mode: replace
-
-      - name: Set job status
-        if: steps.check.outputs.has_special == 'true' && steps.verify.outputs.success == 'false'
+      - name: Prepare bridge outputs
         run: |
-          echo "::error::Commit verification failed. See PR comment for details."
-          exit 1
+          jq -n \
+            --arg has_special "${{ steps.check.outputs.has_special }}" \
+            --arg success "${{ steps.verify.outputs.success }}" \
+            '{
+              has_special: $has_special,
+              success: $success,
+            }' > bridge-outputs.json
+
+      - name: Emit bridge artifact
+        uses: leanprover-community/privilege-escalation-bridge/emit@d3bd99c50a4cf8c5350a211e8e3ba07ac19067d8 # v1.1.0
+        with:
+          artifact: workflow-data
+          outputs_file: bridge-outputs.json
+          include_event: minimal
+          files: |
+            comment_body.md
+          retention_days: 5

.github/workflows/commit_verification_wf_run.yml

@@ -0,0 +1,62 @@
+# Commit Verification CI (workflow run)
+# Verifies transient and automated commits in PRs
+#
+# - Downloads the workflow artifact uploaded by commit_verification.yml
+# - Posts a summary comment categorizing commits for reviewers
+
+name: Commit Verification (workflow_run)
+
+on:
+  workflow_run:
+    workflows: ["Commit Verification"]
+    types:
+      - completed
+
+permissions:
+  actions: read
+  contents: read
+  pull-requests: write
+
+jobs:
+  verify:
+    name: Verify Transient and Automated Commits
+    runs-on: ubuntu-latest
+    if: ${{ github.event.workflow_run.conclusion == 'success' }}
+    steps:
+      - name: Consume bridge artifact
+        id: bridge
+        uses: leanprover-community/privilege-escalation-bridge/consume@d3bd99c50a4cf8c5350a211e8e3ba07ac19067d8 # v1.1.0
+        with:
+          token: ${{ github.token }}
+          artifact: workflow-data
+          source_workflow: Commit Verification
+          require_event: pull_request
+          fail_on_missing: false
+          extract: |
+            pr_number=meta.pr_number
+            has_special=outputs.has_special
+            success=outputs.success
+
+      - name: Find existing comment
+        if: steps.bridge.outputs.has_special == 'true'
+        uses: peter-evans/find-comment@b30e6a3c0ed37e7c023ccd3f1db5c6c0b0c23aad # v4
+        id: find-comment
+        with:
+          issue-number: ${{ steps.bridge.outputs.pr_number }}
+          comment-author: 'github-actions[bot]'
+          body-includes: 'Commit Verification Summary'
+
+      - name: Post or update comment
+        if: steps.bridge.outputs.has_special == 'true'
+        uses: peter-evans/create-or-update-comment@e8674b075228eee787fea43ef493e45ece1004c9 # v4
+        with:
+          comment-id: ${{ steps.find-comment.outputs.comment-id }}
+          issue-number: ${{ steps.bridge.outputs.pr_number }}
+          body-path: .bridge/comment_body.md
+          edit-mode: replace
+
+      - name: Set job status
+        if: steps.bridge.outputs.has_special == 'true' && steps.bridge.outputs.success == 'false'
+        run: |
+          echo "::error::Commit verification failed. See PR comment for details."
+          exit 1

.github/workflows/maintainer_bors_wf_run.yml

@@ -69,14 +69,21 @@ jobs:
       - name: Select bridge or legacy inputs
         id: inputs
         if: ${{ steps.bridge.outputs.pr_number != '' || steps.legacy.outputs.pr_number != '' }}
+        env:
+          INPUT_AUTHOR: ${{ steps.bridge.outputs.author }}${{ steps.legacy.outputs.author }}
+          INPUT_PR_NUMBER: ${{ steps.bridge.outputs.pr_number }}${{ steps.legacy.outputs.pr_number }}
+          INPUT_BOT: ${{ steps.bridge.outputs.bot }}${{ steps.legacy.outputs.bot }}
+          INPUT_REMOVE_LABELS: ${{ steps.bridge.outputs.removeLabels }}${{ steps.legacy.outputs.removeLabels }}
+          INPUT_MORD: ${{ steps.bridge.outputs.mOrD }}${{ steps.legacy.outputs.mOrD }}
+          INPUT_SOURCE: ${{ steps.bridge.outputs.pr_number != '' && 'bridge' || (steps.legacy.outputs.pr_number != '' && 'legacy' || 'none') }}
         run: |
           {
-            echo "author=${{ steps.bridge.outputs.author }}${{ steps.legacy.outputs.author }}"
-            echo "pr_number=${{ steps.bridge.outputs.pr_number }}${{ steps.legacy.outputs.pr_number }}"
-            echo "bot=${{ steps.bridge.outputs.bot }}${{ steps.legacy.outputs.bot }}"
-            echo "removeLabels=${{ steps.bridge.outputs.removeLabels }}${{ steps.legacy.outputs.removeLabels }}"
-            echo "mOrD=${{ steps.bridge.outputs.mOrD }}${{ steps.legacy.outputs.mOrD }}"
-            echo "input_source=${{ steps.bridge.outputs.pr_number != '' && 'bridge' || (steps.legacy.outputs.pr_number != '' && 'legacy' || 'none') }}"
+            echo "author=${INPUT_AUTHOR}"
+            echo "pr_number=${INPUT_PR_NUMBER}"
+            echo "bot=${INPUT_BOT}"
+            echo "removeLabels=${INPUT_REMOVE_LABELS}"
+            echo "mOrD=${INPUT_MORD}"
+            echo "input_source=${INPUT_SOURCE}"
           } | tee -a "$GITHUB_OUTPUT"
 
       - name: Note legacy artifact fallback
@@ -182,6 +189,7 @@ jobs:
         if: ${{ ! steps.inputs.outputs.mOrD == '' &&
           ( steps.user_permission.outputs.require-result == 'true' ||
             steps.inputs.outputs.bot == 'true' ) }}
+        continue-on-error: true
         env:
           ZULIP_API_KEY: ${{ secrets.ZULIP_API_KEY }}
           ZULIP_EMAIL: github-mathlib4-bot@leanprover.zulipchat.com

.github/workflows/maintainer_merge_wf_run.yml

@@ -73,18 +73,28 @@ jobs:
       - name: Select bridge or legacy inputs
         id: inputs
         if: ${{ steps.bridge.outputs.pr_number != '' || steps.legacy.outputs.pr_number != '' }}
+        env:
+          INPUT_AUTHOR: ${{ steps.bridge.outputs.author }}${{ steps.legacy.outputs.author }}
+          INPUT_PR_AUTHOR: ${{ steps.bridge.outputs.pr_author }}${{ steps.legacy.outputs.pr_author }}
+          INPUT_PR_NUMBER: ${{ steps.bridge.outputs.pr_number }}${{ steps.legacy.outputs.pr_number }}
+          INPUT_PR_TITLE: ${{ steps.bridge.outputs.pr_title }}${{ steps.legacy.outputs.pr_title }}
+          INPUT_PR_URL: ${{ steps.bridge.outputs.pr_url }}${{ steps.legacy.outputs.pr_url }}
+          INPUT_EVENT_NAME: ${{ steps.bridge.outputs.event_name }}${{ steps.legacy.outputs.event_name }}
+          INPUT_MORD: ${{ steps.bridge.outputs.mOrD }}${{ steps.legacy.outputs.mOrD }}
+          INPUT_SOURCE: ${{ steps.bridge.outputs.pr_number != '' && 'bridge' || (steps.legacy.outputs.pr_number != '' && 'legacy' || 'none') }}
+          INPUT_COMMENT: ${{ steps.bridge.outputs.comment }}${{ steps.legacy.outputs.comment }}
         run: |
           {
-            echo "author=${{ steps.bridge.outputs.author }}${{ steps.legacy.outputs.author }}"
-            echo "pr_author=${{ steps.bridge.outputs.pr_author }}${{ steps.legacy.outputs.pr_author }}"
-            echo "pr_number=${{ steps.bridge.outputs.pr_number }}${{ steps.legacy.outputs.pr_number }}"
-            echo "pr_title=${{ steps.bridge.outputs.pr_title }}${{ steps.legacy.outputs.pr_title }}"
-            echo "pr_url=${{ steps.bridge.outputs.pr_url }}${{ steps.legacy.outputs.pr_url }}"
-            echo "event_name=${{ steps.bridge.outputs.event_name }}${{ steps.legacy.outputs.event_name }}"
-            echo "mOrD=${{ steps.bridge.outputs.mOrD }}${{ steps.legacy.outputs.mOrD }}"
-            echo "input_source=${{ steps.bridge.outputs.pr_number != '' && 'bridge' || (steps.legacy.outputs.pr_number != '' && 'legacy' || 'none') }}"
+            echo "author=${INPUT_AUTHOR}"
+            echo "pr_author=${INPUT_PR_AUTHOR}"
+            echo "pr_number=${INPUT_PR_NUMBER}"
+            echo "pr_title=${INPUT_PR_TITLE}"
+            echo "pr_url=${INPUT_PR_URL}"
+            echo "event_name=${INPUT_EVENT_NAME}"
+            echo "mOrD=${INPUT_MORD}"
+            echo "input_source=${INPUT_SOURCE}"
           } | tee -a "$GITHUB_OUTPUT"
-          printf 'comment<<EOF\n%s\nEOF\n' "${{ steps.bridge.outputs.comment }}${{ steps.legacy.outputs.comment }}" | tee -a "$GITHUB_OUTPUT"
+          printf 'comment<<EOF\n%s\nEOF\n' "${INPUT_COMMENT}" | tee -a "$GITHUB_OUTPUT"
 
       - name: Note legacy artifact fallback
         if: ${{ steps.inputs.outputs.input_source == 'legacy' }}
@@ -139,7 +149,7 @@ jobs:
           then
             legacy_suffix=" (legacy)"
           fi
-          metadata=$'trigger_name: ['"${trigger_name}"$']('"${trigger_run_url}"$')\nwf_run: [workflow_run]('"${wf_run_url}"$')'"${legacy_suffix}"
+          metadata=$'['"${trigger_name}"$']('"${trigger_run_url}"$'), [wf_run]('"${wf_run_url}"$')'"${legacy_suffix}"
           message="${message}"$'\n\n---\n'"${metadata}"
           printf 'title<<EOF\n%s\nEOF' "${message}" | tee "$GITHUB_OUTPUT"
         env:
@@ -153,6 +163,7 @@ jobs:
 
       - name: Send message on Zulip
         if: ${{ steps.actorTeams.outputs.isTeamMember == 'true' }}
+        continue-on-error: true
         uses: zulip/github-actions-zulip/send-message@e4c8f27c732ba9bd98ac6be0583096dea82feea5 # v1.0.2
         with:
           api-key: ${{ secrets.ZULIP_API_KEY }}
@@ -176,12 +187,13 @@ jobs:
           then
             legacy_suffix=" (legacy)"
           fi
-          metadata=$'trigger_name: ['"${trigger_name}"$']('"${trigger_run_url}"$')\nwf_run: [workflow_run]('"${wf_run_url}"$')'"${legacy_suffix}"
+          metadata=$'['"${trigger_name}"$']('"${trigger_run_url}"$'), [wf_run]('"${wf_run_url}"$')'"${legacy_suffix}"
           body="${body}"$'\n\n---\n'"${metadata}"
           printf 'body<<EOF\n%s\nEOF\n' "${body}" | tee -a "$GITHUB_OUTPUT"
 
       - name: Add comment to PR
         if: ${{ steps.actorTeams.outputs.isTeamMember == 'true' }}
+        continue-on-error: true
         uses: GrantBirki/comment@608e41b19bc973020ec0e189ebfdae935d7fe0cc # v2.1.1
         with:
           # if a comment triggers the action, then `issue.number` is set
@@ -202,6 +214,7 @@ jobs:
 
       - name: Add label to PR
         if: ${{ steps.actorTeams.outputs.isTeamMember == 'true' }}
+        continue-on-error: true
         uses: actions/github-script@ed597411d8f924073f98dfc5c65a23a2325f34cd # v8.0.0
         with:
           # labels added by GITHUB_TOKEN won't trigger the Zulip emoji workflow

.github/workflows/nightly_bump_and_merge.yml

@@ -337,10 +337,13 @@ jobs:
             IFS='|' read -r PR_NUMBER GITHUB_DIFF _ <<< "$MERGE_INFO"
             MESSAGE+="- [lean-pr-testing-${PR_NUMBER}](${GITHUB_DIFF}) (adaptations for lean#${PR_NUMBER})"$'\n\n'
             MESSAGE+=$'```bash\n'
-            MESSAGE+=$'tmp=$(mktemp)\n'
-            MESSAGE+=$'wget -qO "$tmp" https://raw.githubusercontent.com/leanprover-community/mathlib-ci/${{ steps.get_mathlib_ci.outputs.ref }}/scripts/nightly/merge-lean-testing-pr.sh\n'
-            MESSAGE+=$'chmod +x "$tmp"\n'
-            MESSAGE+="\"\$tmp\" ${PR_NUMBER}"$'\n'
+            MESSAGE+=$'tmpscript=$(mktemp)\n'
+            MESSAGE+=$'wget -qO "$tmpscript" https://raw.githubusercontent.com/leanprover-community/mathlib-ci/${{ steps.get_mathlib_ci.outputs.ref }}/scripts/nightly/merge-lean-testing-pr.sh\n'
+            MESSAGE+=$'chmod +x "$tmpscript"\n'
+            MESSAGE+=$'tmpdir=$(mktemp -d)\n'
+            MESSAGE+=$'git clone --depth=1 --filter=blob:none https://github.com/leanprover-community/mathlib4 "$tmpdir"\n'
+            MESSAGE+=$'cd "$tmpdir"\n'
+            MESSAGE+="\"\$tmpscript\" ${PR_NUMBER}"$'\n'
             MESSAGE+=$'```\n\n'
           done
         else

.github/workflows/nightly_detect_failure.yml

@@ -431,8 +431,8 @@ jobs:
             bump_branch_suffix = bump_branch.replace('bump/', '')
             failed_link = f"https://github.com/{repository}/actions/runs/{current_run_id}"
             payload = f"🛠️: Automatic PR creation [failed]({failed_link}). Please create a new bump/nightly-{current_version} branch from nightly-testing (specifically {sha}), and then PR that to {bump_branch}. "
-            payload += "To do so semi-automatically from a mathlib checkout, run:\n\n"
-            payload += f"```bash\ntmp=$(mktemp)\nwget -qO \"$tmp\" https://raw.githubusercontent.com/leanprover-community/mathlib-ci/${{ steps.get_mathlib_ci.outputs.ref }}/scripts/nightly/create-adaptation-pr.sh\nchmod +x \"$tmp\"\n\"$tmp\" --bumpversion={bump_branch_suffix} --nightlydate={current_version} --nightlysha={sha}\n```\n"
+            payload += "To do so semi-automatically, run:\n\n"
+            payload += f"```bash\ntmpscript=$(mktemp)\nwget -qO \"$tmpscript\" https://raw.githubusercontent.com/leanprover-community/mathlib-ci/${{ steps.get_mathlib_ci.outputs.ref }}/scripts/nightly/create-adaptation-pr.sh\nchmod +x \"$tmpscript\"\ntmpdir=$(mktemp -d)\ngit clone --filter=blob:none https://github.com/leanprover-community/mathlib4 \"$tmpdir\"\ncd \"$tmpdir\"\n\"$tmpscript\" --bumpversion={bump_branch_suffix} --nightlydate={current_version} --nightlysha={sha}\n```\n"
             # Check if we already posted a message for this nightly date and bump branch.
             # We extract these fields from the last bot message rather than comparing substrings,
             # since the message also contains a run ID that differs between workflow runs.

.github/workflows/zulip_emoji_ci_status.yaml

@@ -98,6 +98,7 @@ jobs:
 
     - name: Update CI emoji
       if: steps.pr.outputs.skip != 'true' && steps.action.outputs.ci_action != 'skip'
+      continue-on-error: true
       env:
         ZULIP_API_KEY: ${{ secrets.ZULIP_API_KEY }}
         ZULIP_EMAIL: github-mathlib4-bot@leanprover.zulipchat.com

.github/workflows/zulip_emoji_closed_pr.yaml

@@ -61,6 +61,7 @@ jobs:
       - name: Update zulip emoji reactions
         if: ${{ ! startsWith(github.event.pull_request.title, '[Merged by Bors]') ||
                 github.event_name == 'reopened' }}
+        continue-on-error: true
         env:
           ZULIP_API_KEY: ${{ secrets.ZULIP_API_KEY }}
           ZULIP_EMAIL: github-mathlib4-bot@leanprover.zulipchat.com

.github/workflows/zulip_emoji_labelling.yaml

@@ -37,6 +37,7 @@ jobs:
         pip install -r "$CI_SCRIPTS_DIR/zulip/requirements.txt"
 
     - name: Add or remove emoji
+      continue-on-error: true  # Emoji updates are cosmetic; never fail CI over them
       env:
         ZULIP_API_KEY: ${{ secrets.ZULIP_API_KEY }}
         ZULIP_EMAIL: github-mathlib4-bot@leanprover.zulipchat.com