Merge branch 'master' into liminfmulconst

Author: CoolRmal

.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: d7b053bde8ef240c29f6724fa285dc5bb6bbe00a
   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

@@ -247,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
@@ -327,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
@@ -380,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 --skip-proofwidgets get
-              # Run again with --repo, to ensure we actually get the oleans.
-              ../tools-branch/.lake/build/bin/cache --repo="$CACHE_REPO" --skip-proofwidgets 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
@@ -396,18 +332,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
@@ -462,8 +390,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
@@ -646,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 }}
@@ -708,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
@@ -815,6 +743,12 @@ jobs:
       - name: clean up the import graph file
         run: rm import_graph.dot
 
+      - name: check all scripts build successfully
+        run: |
+          lake env lean scripts/create_deprecated_modules.lean
+          lake env lean scripts/autolabel.lean
+          lake exe check_title_labels --labels "t-algebra" "feat: dummy PR for testing"
+
       - name: build everything
         # make sure everything is available for test/import_all.lean
         # and that miscellaneous executables still work
@@ -937,7 +871,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
@@ -952,7 +887,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/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: |