Merge branch 'master' into Frullani_integral

Author: Deep0Thinking

.github/actions/get-mathlib-ci/README.md

@@ -9,7 +9,8 @@ Any workflow that needs `mathlib-ci` should use this action instead of writing i
 own `actions/checkout` block for `leanprover-community/mathlib-ci`.
 
 The default `ref` in [`action.yml`](./action.yml) is the single canonical pinned
-`mathlib-ci` commit for this repository.
+`mathlib-ci` commit for this repository. This is auto-updated regularly by the
+[`update_dependencies.yml` workflow](../../workflows/update_dependencies.yml).
 
 ## Why
 

.github/actions/get-mathlib-ci/action.yml

@@ -9,7 +9,8 @@ inputs:
     required: false
     # Default pinned commit used by workflows unless they explicitly override.
     # Update this ref as needed to pick up changes to mathlib-ci scripts
-    default: 261ca4c0c6bd3267e4846ef9fdd676afab9fef4e
+    # This is also updated automatically by .github/workflows/update_dependencies.yml
+    default: b6def9edd1c39de8602b8c177c66e9416e5dbc60
   path:
     description: Checkout destination path.
     required: false

.github/workflows/actionlint.yml

@@ -12,7 +12,7 @@ jobs:
         uses: actions/checkout@de0fac2e4500dabe0009e67214ff5f5447ce83dd # v6.0.2
 
       - name: suggester / actionlint
-        uses: reviewdog/action-actionlint@0d952c597ef8459f634d7145b0b044a9699e5e43 # v1.71.0
+        uses: reviewdog/action-actionlint@6fb7acc99f4a1008869fa8a0f09cfca740837d9d # v1.72.0
         with:
           tool_name: actionlint
           fail_level: any

.github/workflows/build_template.yml

@@ -310,13 +310,19 @@ jobs:
             # cf. https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/Mathlib.20has.20moved.20to.20the.20new.20module.20system/near/563452000
             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 get
-              # Run again with --repo, to ensure we actually get the oleans.
-              ../tools-branch/.lake/build/bin/cache --repo="$CACHE_REPO" get
-
-              echo "Switching back to branch head"
-              git checkout "$ORIG_SHA"
+              # Skip warmup if the previous commit uses a different toolchain
+              PREV_TOOLCHAIN=$(git show "$PREV_SHA:lean-toolchain" 2>/dev/null || true)
+              if [[ "$PREV_TOOLCHAIN" != "$(cat lean-toolchain)" ]]; then
+                echo "Previous commit $PREV_SHA uses a different toolchain ($PREV_TOOLCHAIN); skipping warmup."
+              else
+                git checkout "$PREV_SHA"
+                ../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" get
+
+                echo "Switching back to branch head"
+                git checkout "$ORIG_SHA"
+              fi
             else
               echo "Could not fetch $PREV_SHA; skipping parent warmup cache fetch."
             fi
@@ -568,7 +574,7 @@ jobs:
       - name: Generate lean-pr-testing app token
         if: ${{ always() && github.repository == 'leanprover-community/mathlib4-nightly-testing' && (startsWith(github.ref_name, 'lean-pr-testing-') || startsWith(github.ref_name, 'batteries-pr-testing-')) }}
         id: lean-pr-testing-token
-        uses: actions/create-github-app-token@29824e69f54612133e76f7eaac726eef6c875baf # v2.2.1
+        uses: actions/create-github-app-token@f8d387b68d61c58ab83c6c016672934102569859 # v3.0.0
         with:
           app-id: ${{ secrets.MATHLIB_LEAN_PR_TESTING_APP_ID }}
           private-key: ${{ secrets.MATHLIB_LEAN_PR_TESTING_PRIVATE_KEY }}
@@ -630,7 +636,7 @@ jobs:
           echo "CACHE_BIN=$CACHE_BIN" >> "$GITHUB_ENV"
 
       - name: Download cache staging artifact
-        uses: actions/download-artifact@70fc10c6e5e1ce46ad2ea6f2b72d43f7d47b13c3 # v8.0.0
+        uses: actions/download-artifact@3e5f45b2cfb9172054b4087a40e8e0b5a5461e7c # v8.0.1
         with:
           name: cache-staging
           path: cache-staging

.github/workflows/check_pr_titles.yaml

@@ -70,7 +70,7 @@ jobs:
           fi
 
       - name: Add comment to fix PR title
-        uses: marocchino/sticky-pull-request-comment@773744901bac0e8cbb5a0dc842800d45e9b2b405 # v2.9.4
+        uses: marocchino/sticky-pull-request-comment@70d2764d1a7d5d9560b100cbea0077fc8f633987 # v3.0.2
         if: failure() && steps.pr-title-check.outputs.errors
         with:
           header: 'PR Title Check'
@@ -120,7 +120,7 @@ jobs:
 
       - name: Add comment that PR title is fixed
         if: steps.pr-title-check.outcome == 'success'
-        uses: marocchino/sticky-pull-request-comment@773744901bac0e8cbb5a0dc842800d45e9b2b405 # v2.9.4
+        uses: marocchino/sticky-pull-request-comment@70d2764d1a7d5d9560b100cbea0077fc8f633987 # v3.0.2
         with:
           header: 'PR Title Check'
           # should do nothing if a 'PR Title Check' comment does not exist

.github/workflows/commit_verification.yml

@@ -111,7 +111,7 @@ jobs:
             }' > bridge-outputs.json
 
       - name: Emit bridge artifact
-        uses: leanprover-community/privilege-escalation-bridge/emit@d3bd99c50a4cf8c5350a211e8e3ba07ac19067d8 # v1.1.0
+        uses: leanprover-community/privilege-escalation-bridge/emit@f5dfe313a79647c07315b451b2dc2a81a161a50d # v1.2.0
         with:
           artifact: workflow-data
           outputs_file: bridge-outputs.json

.github/workflows/commit_verification_wf_run.yml

@@ -25,7 +25,7 @@ jobs:
     steps:
       - name: Consume bridge artifact
         id: bridge
-        uses: leanprover-community/privilege-escalation-bridge/consume@d3bd99c50a4cf8c5350a211e8e3ba07ac19067d8 # v1.1.0
+        uses: leanprover-community/privilege-escalation-bridge/consume@f5dfe313a79647c07315b451b2dc2a81a161a50d # v1.2.0
         with:
           token: ${{ github.token }}
           artifact: workflow-data

.github/workflows/dependent-issues.yml

@@ -12,7 +12,7 @@ jobs:
     if: github.repository == 'leanprover-community/mathlib4'
     # timeout-minutes: 3
     steps:
-      - uses: styfle/cancel-workflow-action@3155a141048f8f89c06b4cdae32e7853e97536bc # 0.13.0
+      - uses: styfle/cancel-workflow-action@d07a454dad7609a92316b57b23c9ccfd4f59af66 # 0.13.1
         with:
           all_but_latest: true
           access_token: ${{ github.token }}

.github/workflows/export_telemetry.yaml

@@ -19,7 +19,7 @@ jobs:
     runs-on: ubuntu-latest
     steps:
       - name: Export workflow telemetry
-        uses: corentinmusard/otel-cicd-action@0f9f16fceb53fd8c996042e28c642ec61f844876 # v4.0.0
+        uses: corentinmusard/otel-cicd-action@f2d88ecf54d9dd3e01ea95e25f93603212ee93d3 # v4.0.1
         with:
           otlpEndpoint: ${{ vars.OTLP_ENDPOINT }}
           otlpHeaders: ${{ secrets.OTLP_HEADERS }}

.github/workflows/label_new_contributor.yml

@@ -99,7 +99,7 @@ jobs:
 
       - name: Post welcome comment for new contributor
         if: steps.contributor-check.outputs.should_welcome == 'true'
-        uses: marocchino/sticky-pull-request-comment@773744901bac0e8cbb5a0dc842800d45e9b2b405 # v2.9.4
+        uses: marocchino/sticky-pull-request-comment@70d2764d1a7d5d9560b100cbea0077fc8f633987 # v3.0.2
         with:
           header: 'New Contributor Welcome'
           message: |