Merge branch 'master' into Frullani_integral

Author: Deep0Thinking

.github/workflows/PR_summary.yml

@@ -228,7 +228,7 @@ jobs:
         then
           # Format each changed workflow path as a Markdown bullet: "- `path`"
           workflowFilesChangedMarkdown="$(sed "s|^|- \`|; s|\$|\`|" <<< "${workflowFilesChanged}")"
-          workflowDocsReminder="$(printf "### Workflow documentation reminder\nThis PR modifies files under \`.github/workflows/\`.\nPlease update \`docs/workflows.md\` if the workflow inventory, triggers, or behavior changed.\n\nModified workflow files:\n%s\n" "${workflowFilesChangedMarkdown}")"
+          workflowDocsReminder="$(printf "### ⚠️ Workflow documentation reminder\nThis PR modifies files under \`.github/workflows/\`.\nPlease update \`docs/workflows.md\` if the workflow inventory, triggers, or behavior changed.\n\nModified workflow files:\n%s\n" "${workflowFilesChangedMarkdown}")"
         else
           workflowDocsReminder=""
         fi
@@ -239,7 +239,7 @@ jobs:
         then
           # Format each added scripts path as a Markdown bullet: "- `path`"
           scriptsFilesAddedMarkdown="$(sed "s|^|- \`|; s|\$|\`|" <<< "${scriptsFilesAdded}")"
-          scriptsLocationReminder="$(printf "### Scripts folder reminder\nThis PR adds files under \`scripts/\`.\nPlease consider whether each added script belongs in this repository or in \`leanprover-community/mathlib-ci\`.\n\nAdded scripts files:\n%s\n" "${scriptsFilesAddedMarkdown}")"
+          scriptsLocationReminder="$(printf "### ⚠️ Scripts folder reminder\nThis PR adds files under \`scripts/\`.\nPlease consider whether each added script belongs in this repository or in [\`leanprover-community/mathlib-ci\`](https://github.com/leanprover-community/mathlib-ci).\n\nA script belongs in **\`mathlib-ci\`** if it is a CI automation script that interacts with GitHub (e.g. managing labels, posting comments, triggering bots), runs from a trusted external checkout in CI, or requires access to secrets.\n\nA script belongs in **this repository** (\`scripts/\`) if it is a developer or maintainer tool to be run locally, a code maintenance or analysis utility, a style linting tool, or a data file used by the library's own linters.\n\nSee the [\`mathlib-ci\` README](https://github.com/leanprover-community/mathlib-ci) for more details.\n\nAdded scripts files:\n%s\n" "${scriptsFilesAddedMarkdown}")"
         else
           scriptsLocationReminder=""
         fi

.github/workflows/bors.yml

@@ -27,6 +27,9 @@ jobs:
     with:
       concurrency_group: ${{ github.workflow }}-${{ github.ref }}-${{ github.run_id }}
       pr_branch_ref: ${{ github.sha }}
+      # Use the MASTER cache key only when merging into mathlib4 (staging branch);
+      # 'bors try' runs (trying branch) and nightly-testing use NON_MASTER
+      cache_application_id: ${{ github.ref_name == 'staging' && github.repository == 'leanprover-community/mathlib4' && vars.CACHE_MASTER_WRITER_AZURE_APP_ID || vars.CACHE_NON_MASTER_WRITER_AZURE_APP_ID }}
       # bors runs should build the tools from their commit-under-test: after all, we are trying to
       # test 'what would happen if this was merged', so we need to use the 'would-be-post-merge' tools
       tools_branch_ref: ${{ github.sha }}

.github/workflows/build.yml

@@ -35,5 +35,7 @@ jobs:
     with:
       concurrency_group: ${{ github.workflow }}-${{ github.ref }}-${{ (github.event_name == 'push' && github.ref == 'refs/heads/master' && github.run_id) || '' }}
       pr_branch_ref: ${{ github.sha }}
+      # Use the MASTER cache key only on mathlib4/master; nightly-testing and other branches use NON_MASTER
+      cache_application_id: ${{ github.repository == 'leanprover-community/mathlib4' && github.ref == 'refs/heads/master' && vars.CACHE_MASTER_WRITER_AZURE_APP_ID || vars.CACHE_NON_MASTER_WRITER_AZURE_APP_ID }}
       runs_on: pr
     secrets: inherit

.github/workflows/build_fork.yml

@@ -36,5 +36,6 @@ jobs:
     with:
       concurrency_group: ${{ github.workflow }}-${{ github.event.pull_request.number }}
       pr_branch_ref: ${{ github.event.pull_request.head.sha }}
+      cache_application_id: ${{ vars.CACHE_NON_MASTER_WRITER_AZURE_APP_ID }}
       runs_on: pr
     secrets: inherit

.github/workflows/build_template.yml

@@ -24,6 +24,9 @@ on:
         type: string
         required: false
         default: ''
+      cache_application_id:
+        type: string
+        required: true
 
 env:
   # Disable Lake's automatic fetching of cloud builds.
@@ -244,76 +247,6 @@ jobs:
             echo "✅ All inputRevs in lake-manifest.json are valid"
           fi
 
-      - name: validate ProofWidgets source repository
-        # Only enforce this on the main mathlib4 repository, not on nightly-testing
-        if: github.repository == 'leanprover-community/mathlib4'
-        shell: bash
-        run: |
-          cd pr-branch
-
-          expected_url='https://github.com/leanprover-community/ProofWidgets4'
-          proofwidgets_count=$(jq '[.packages[] | select(.name == "proofwidgets")] | length' lake-manifest.json)
-          if [ "$proofwidgets_count" -ne 1 ]; then
-            echo "❌ Error: expected exactly one proofwidgets entry in lake-manifest.json, found $proofwidgets_count"
-            exit 1
-          fi
-
-          proofwidgets_url=$(jq -r '.packages[] | select(.name == "proofwidgets") | .url' lake-manifest.json)
-          normalized_url="${proofwidgets_url%.git}"
-          if [ "$normalized_url" != "$expected_url" ]; then
-            echo "❌ Error: invalid ProofWidgets source URL in lake-manifest.json"
-            echo "  expected: $expected_url"
-            echo "  found:    $proofwidgets_url"
-            exit 1
-          fi
-
-          echo "✅ ProofWidgets source URL is allowed: $proofwidgets_url"
-
-      - name: verify ProofWidgets lean-toolchain matches on versioned releases
-        # Only enforce this on the main mathlib4 repository, not on nightly-testing
-        if: github.repository == 'leanprover-community/mathlib4'
-        shell: bash
-        run: |
-          cd pr-branch
-
-          # Read the lean-toolchain file
-          TOOLCHAIN=$(cat lean-toolchain | tr -d '[:space:]')
-          echo "Lean toolchain: $TOOLCHAIN"
-
-          # Check if toolchain matches the versioned release pattern: leanprover/lean4:vX.Y.Z (with optional suffix like -rc1)
-          if [[ "$TOOLCHAIN" =~ ^leanprover/lean4:v[0-9]+\.[0-9]+\.[0-9]+(-[a-zA-Z0-9.-]+)?$ ]]; then
-            echo "✓ Detected versioned Lean release: $TOOLCHAIN"
-            echo "Verifying ProofWidgets lean-toolchain matches..."
-
-            # Check if ProofWidgets lean-toolchain exists
-            if [ ! -f .lake/packages/proofwidgets/lean-toolchain ]; then
-              echo "❌ Error: .lake/packages/proofwidgets/lean-toolchain does not exist"
-              echo "This file should be created by 'lake env' during dependency download."
-              exit 1
-            fi
-
-            # Read ProofWidgets lean-toolchain
-            PROOFWIDGETS_TOOLCHAIN=$(cat .lake/packages/proofwidgets/lean-toolchain | tr -d '[:space:]')
-            echo "ProofWidgets toolchain: $PROOFWIDGETS_TOOLCHAIN"
-
-            # Compare the two
-            if [ "$TOOLCHAIN" != "$PROOFWIDGETS_TOOLCHAIN" ]; then
-              echo "❌ Error: Lean toolchain mismatch!"
-              echo "  Main lean-toolchain: $TOOLCHAIN"
-              echo "  ProofWidgets lean-toolchain: $PROOFWIDGETS_TOOLCHAIN"
-              echo ""
-              echo "When using a versioned Lean release (leanprover/lean4:vX.Y.Z),"
-              echo "the ProofWidgets dependency must use the same toolchain."
-              echo "Please update the ProofWidgets dependency to use $TOOLCHAIN"
-              exit 1
-            else
-              echo "✅ ProofWidgets lean-toolchain matches: $TOOLCHAIN"
-            fi
-          else
-            echo "ℹ Lean toolchain is not a versioned release (pattern: leanprover/lean4:vX.Y.Z)"
-            echo "Skipping ProofWidgets toolchain verification."
-          fi
-
       - name: get cache (1/3 - setup and initial fetch)
         id: get_cache_part1_setup
         shell: bash # only runs `cache get` from `tools-branch`, so doesn't need to be inside landrun
@@ -324,7 +257,7 @@ jobs:
 
           # Fail quickly if the cache is completely cold, by checking for Mathlib.Init
           echo "Attempting to fetch olean for Mathlib/Init.lean from cache..."
-          ../tools-branch/.lake/build/bin/cache --skip-proofwidgets get Mathlib/Init.lean
+          ../tools-branch/.lake/build/bin/cache get Mathlib/Init.lean
 
       - name: get cache (2/3 - test Mathlib.Init cache)
         id: get_cache_part2_test
@@ -378,9 +311,9 @@ jobs:
             echo "Warming up cache using previous commit: $PREV_SHA (source: $PREV_SHA_SOURCE)"
             if git cat-file -e "$PREV_SHA^{commit}" 2>/dev/null || git fetch --no-tags --depth=1 origin "$PREV_SHA"; then
               git checkout "$PREV_SHA"
-              ../tools-branch/.lake/build/bin/cache --skip-proofwidgets get
+              ../tools-branch/.lake/build/bin/cache get
               # Run again with --repo, to ensure we actually get the oleans.
-              ../tools-branch/.lake/build/bin/cache --repo="$CACHE_REPO" --skip-proofwidgets get
+              ../tools-branch/.lake/build/bin/cache --repo="$CACHE_REPO" get
 
               echo "Switching back to branch head"
               git checkout "$ORIG_SHA"
@@ -393,18 +326,10 @@ jobs:
 
           echo "Fetching all remaining cache..."
 
-          ../tools-branch/.lake/build/bin/cache --skip-proofwidgets get
+          ../tools-branch/.lake/build/bin/cache get
 
           # Run again with --repo, to ensure we actually get the oleans.
-          ../tools-branch/.lake/build/bin/cache --repo="$CACHE_REPO" --skip-proofwidgets get
-
-      - name: fetch ProofWidgets release
-        # We need network access for ProofWidgets frontend assets.
-        # Run inside landrun so PR-controlled code remains sandboxed.
-        shell: landrun --unrestricted-network --rox /etc --rox /usr --rw /dev --rox /home/lean/.elan --rox /home/lean/actions-runner/_work --rw pr-branch/.lake/ --env PATH --env HOME --env GITHUB_OUTPUT --env CI -- bash -euxo pipefail {0}
-        run: |
-          cd pr-branch
-          lake build proofwidgets:release
+          ../tools-branch/.lake/build/bin/cache --repo="$CACHE_REPO" get
 
       - name: update {Mathlib, Tactic, Counterexamples, Archive}.lean
         id: mk_all
@@ -459,8 +384,8 @@ jobs:
         shell: bash
         run: |
           cd pr-branch
-          ../tools-branch/.lake/build/bin/cache --skip-proofwidgets get Archive.lean
-          ../tools-branch/.lake/build/bin/cache --skip-proofwidgets get Counterexamples.lean
+          ../tools-branch/.lake/build/bin/cache get Archive.lean
+          ../tools-branch/.lake/build/bin/cache get Counterexamples.lean
 
       - name: build archive
         id: archive
@@ -672,6 +597,9 @@ jobs:
     name: Upload to cache
     needs: [build]
     runs-on: ubuntu-latest # These steps run on a GitHub runner; no landrun sandboxing is needed.
+    permissions:
+      contents: read
+      id-token: write
     # We only upload the cache if the build started (whether succeeding, failing, or cancelled)
     # but not if any earlier step failed or was cancelled.
     # See discussion at https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/Some.20files.20not.20found.20in.20the.20cache/near/407183836
@@ -707,16 +635,41 @@ jobs:
           name: cache-staging
           path: cache-staging
 
-      - name: Upload staged cache to Azure
+      - name: Azure CLI OIDC login and mint storage bearer token
+        id: mint_cache_bearer
+        continue-on-error: true
+        uses: leanprover-community/mathlib-ci/.github/actions/azure-create-cache-token@17db5ff55a65df98d55cbddcc67938f70d10dab2
+        with:
+          azure-client-id: ${{ inputs.cache_application_id }}
+          azure-tenant-id: ${{ secrets.LPC_AZ_TENANT_ID }}
+
+      - name: Fallback to SAS token if bearer mint fails (for ease of migration)
+        if: ${{ steps.mint_cache_bearer.outcome != 'success' }}
         shell: bash
+        env:
+          MATHLIB_CACHE_SAS_RAW: ${{ secrets.MATHLIB_CACHE_SAS }}
         run: |
-          # Trim trailing whitespace from secrets to prevent issues with accidentally added spaces
-          export MATHLIB_CACHE_SAS="${MATHLIB_CACHE_SAS_RAW%"${MATHLIB_CACHE_SAS_RAW##*[![:space:]]}"}"
+          if [ -z "$MATHLIB_CACHE_SAS_RAW" ]; then
+            echo "Azure bearer mint failed and secrets.MATHLIB_CACHE_SAS is not set"
+            exit 1
+          fi
+
+          MATHLIB_CACHE_SAS="${MATHLIB_CACHE_SAS_RAW%"${MATHLIB_CACHE_SAS_RAW##*[![:space:]]}"}"
+          if [ -z "$MATHLIB_CACHE_SAS" ]; then
+            echo "Azure bearer mint failed and secrets.MATHLIB_CACHE_SAS is empty after trimming"
+            exit 1
+          fi
 
+          echo "::add-mask::$MATHLIB_CACHE_SAS"
+          echo "MATHLIB_CACHE_AZURE_BEARER_TOKEN=" >> "$GITHUB_ENV"
+          echo "MATHLIB_CACHE_SAS=$MATHLIB_CACHE_SAS" >> "$GITHUB_ENV"
+          echo "Using SAS fallback because bearer mint step failed."
+
+      - name: Upload staged cache to Azure
+        shell: bash
+        run: |
           echo "Uploading cache to Azure..."
           MATHLIB_CACHE_USE_CLOUDFLARE=0 lake env "$CACHE_BIN" put-staged --staging-dir="cache-staging" --repo=${{ github.event.pull_request.head.repo.full_name || github.repository }}
-        env:
-          MATHLIB_CACHE_SAS_RAW: ${{ secrets.MATHLIB_CACHE_SAS }}
 
   post_steps:
     name: Post-Build Step
@@ -816,17 +769,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 +778,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 +787,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)
@@ -915,7 +859,8 @@ jobs:
       - if: >- # bot usernames will cause this step to error with "Could not resolve to a User..."
           contains(steps.PR.outputs.pr_labels, 'auto-merge-after-CI') &&
           steps.get-label-actor.outputs.username != 'mathlib-nolints' &&
-          steps.get-label-actor.outputs.username != 'mathlib-update-dependencies'
+          steps.get-label-actor.outputs.username != 'mathlib-update-dependencies' &&
+          steps.get-label-actor.outputs.username != 'mathlib-splicebot'
         name: check team membership
         uses: tspascoal/get-user-teams-membership@57e9f42acd78f4d0f496b3be4368fc5f62696662 # v3.0.0
         id: actorTeams
@@ -930,7 +875,9 @@ jobs:
           (
             steps.get-label-actor.outputs.username == 'mathlib-nolints' ||
             steps.get-label-actor.outputs.username == 'mathlib-update-dependencies' ||
+            steps.get-label-actor.outputs.username == 'mathlib-splicebot' ||
             contains(steps.actorTeams.outputs.teams, 'mathlib-maintainers') ||
+            contains(steps.actorTeams.outputs.teams, 'lean-release-managers') ||
             contains(steps.actorTeams.outputs.teams, 'bot-users')
           )
         name: If `auto-merge-after-CI` is present, add a `bors merge` comment.

.github/workflows/ci_dev.yml

@@ -45,5 +45,6 @@ jobs:
       pr_branch_ref: ${{ inputs.pr_branch_ref != '' && inputs.pr_branch_ref || github.sha }}
       run_post_ci: ${{ inputs.run_post_ci }}
       mathlib_ci_ref: ${{ inputs.mathlib_ci_ref }}
+      cache_application_id: ${{ vars.CACHE_NON_MASTER_WRITER_AZURE_APP_ID }}
       runs_on: pr
     secrets: inherit