Update lean-toolchain for leanprover/lean4#12490

Author: leanprover-community-mathlib4-bot

.github/workflows/actionlint.yml

@@ -16,4 +16,4 @@ jobs:
         uses: reviewdog/action-actionlint@e58ee9d111489c31395fbe4857b0be6e7635dbda # v1.70.0
         with:
           tool_name: actionlint
-          fail_level: error
+          fail_level: any

.github/workflows/build_template.yml

@@ -37,6 +37,7 @@ jobs:
       build-outcome: ${{ steps.build.outcome }}
       archive-outcome: ${{ steps.archive.outcome }}
       counterexamples-outcome: ${{ steps.counterexamples.outcome }}
+      cache-staging-has-files: ${{ steps.cache_staging_check.outputs.has_files }}
       get-cache-outcome: ${{ steps.get.outcome }}
       lint-outcome: ${{ steps.lint.outcome }}
       mk_all-outcome: ${{ steps.mk_all.outcome }}
@@ -367,31 +368,6 @@ jobs:
           cd pr-branch
           du .lake/build/lib/lean/Mathlib || echo "This code should be unreachable"
 
-      # The cache secrets are available here, so we must not run any untrusted code.
-      - name: Upload cache to Azure
-        # 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
-        if: ${{ always() && steps.get.outcome == 'success' }}
-        shell: bash
-        run: |
-          cd pr-branch
-
-          # 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:]]}"}"
-
-          # Use the trusted cache tool from tools-branch
-          # TODO: this is not doing anything currently, and needs to be integrated with put-unpacked
-          # ../tools-branch/.lake/build/bin/cache commit || true
-          # run this in CI if it gets an incorrect lake hash for existing cache files somehow
-          # ../tools-branch/.lake/build/bin/cache put!
-          # do not try to upload files just downloaded
-
-          echo "Uploading cache to Azure..."
-          MATHLIB_CACHE_USE_CLOUDFLARE=0 ../tools-branch/.lake/build/bin/cache --repo=${{ github.event.pull_request.head.repo.full_name || github.repository }} put-unpacked
-        env:
-          MATHLIB_CACHE_SAS_RAW: ${{ secrets.MATHLIB_CACHE_SAS }}
-
       # Note: we should not be including `Archive` and `Counterexamples` in the cache.
       # We do this for now for the sake of not rebuilding them in every CI run
       # even when they are not touched.
@@ -423,6 +399,47 @@ jobs:
           ../tools-branch/scripts/lake-build-with-retry.sh Counterexamples
           # results of build at pr-branch/.lake/build_summary_Counterexamples.json
 
+      - name: stage Mathlib cache files
+        if: ${{ always() && (steps.build.outcome == 'success' || steps.build.outcome == 'failure' || steps.build.outcome == 'cancelled') }}
+        shell: bash
+        run: |
+          rm -rf cache-staging
+          mkdir -p cache-staging
+          cd pr-branch
+          lake env ../tools-branch/.lake/build/bin/cache --staging-dir="../cache-staging" stage
+
+      - name: stage Archive cache files
+        if: ${{ steps.archive.outcome == 'success' }}
+        shell: bash
+        run: |
+          cd pr-branch
+          lake env ../tools-branch/.lake/build/bin/cache --staging-dir="../cache-staging" stage Archive.lean
+
+      - name: stage Counterexamples cache files
+        if: ${{ steps.counterexamples.outcome == 'success' }}
+        shell: bash
+        run: |
+          cd pr-branch
+          lake env ../tools-branch/.lake/build/bin/cache --staging-dir="../cache-staging" stage Counterexamples.lean
+
+      - name: check cache staging contents
+        id: cache_staging_check
+        if: ${{ always() && (steps.build.outcome == 'success' || steps.build.outcome == 'failure' || steps.build.outcome == 'cancelled') }}
+        shell: bash
+        run: |
+          if find cache-staging -type f -name '*.ltar' -print -quit | grep -q .; then
+            echo "has_files=true" >> "$GITHUB_OUTPUT"
+          else
+            echo "has_files=false" >> "$GITHUB_OUTPUT"
+          fi
+
+      - name: upload cache staging artifact
+        if: ${{ always() && steps.cache_staging_check.outputs.has_files == 'true' }}
+        uses: actions/upload-artifact@b7c566a772e6b6bfb58ed0dc250532a479d7789f # v6.0.0
+        with:
+          name: cache-staging
+          path: cache-staging/
+
       - name: Check if building Archive or Counterexamples failed
         if: steps.archive.outcome == 'failure' || steps.counterexamples.outcome == 'failure'
         run: |
@@ -434,21 +451,6 @@ jobs:
           fi
           exit 1
 
-      # The cache secrets are available here, so we must not run any untrusted code.
-      - name: Upload Archive and Counterexamples cache to Azure
-        shell: bash
-        run: |
-          cd pr-branch
-
-          # 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:]]}"}"
-
-          echo "Uploading Archive and Counterexamples cache to Azure..."
-          MATHLIB_CACHE_USE_CLOUDFLARE=0 ../tools-branch/.lake/build/bin/cache --repo=${{ github.event.pull_request.head.repo.full_name || github.repository }} put-unpacked Archive.lean
-          MATHLIB_CACHE_USE_CLOUDFLARE=0 ../tools-branch/.lake/build/bin/cache --repo=${{ github.event.pull_request.head.repo.full_name || github.repository }} put-unpacked Counterexamples.lean
-        env:
-          MATHLIB_CACHE_SAS_RAW: ${{ secrets.MATHLIB_CACHE_SAS }}
-
       - name: Check {Mathlib, Tactic, Counterexamples, Archive}.lean
         if: ${{ always() && steps.mk_all.outcome != 'skipped' }}
         run: |
@@ -595,9 +597,60 @@ jobs:
           tools-branch/scripts/lean-pr-testing-comments.sh lean
           tools-branch/scripts/lean-pr-testing-comments.sh batteries
 
+  upload_cache:
+    name: Upload to cache
+    needs: [build]
+    runs-on: ubuntu-latest # These steps run on a GitHub runner; no landrun sandboxing is needed.
+    # 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
+    if: ${{ always() && needs.build.outputs.cache-staging-has-files == 'true' }}
+    steps:
+      - name: Checkout tools branch
+        uses: actions/checkout@de0fac2e4500dabe0009e67214ff5f5447ce83dd # v6.0.2
+        with:
+          ref: ${{ inputs.tools_branch_ref != '' && inputs.tools_branch_ref || (github.repository == 'leanprover-community/mathlib4-nightly-testing' && 'nightly-testing-green' || 'master') }}
+          fetch-depth: 1
+
+      - name: Configure Lean
+        uses: leanprover/lean-action@c544e89643240c6b398f14a431bcdc6309e36b3e # v1.4.0
+        with:
+          auto-config: false # Don't run `lake build`, `lake test`, or `lake lint` automatically.
+          use-github-cache: false
+          use-mathlib-cache: false # This can be re-enabled once we are confident in the cache again.
+          reinstall-transient-toolchain: true
+
+      - name: build cache executable
+        run: |
+          lake build cache
+          CACHE_BIN="$(pwd)/.lake/build/bin/cache"
+          if [ ! -x "$CACHE_BIN" ]; then
+            echo "cache binary not found: $CACHE_BIN"
+            exit 1
+          fi
+          echo "CACHE_BIN=$CACHE_BIN" >> "$GITHUB_ENV"
+
+      - name: Download cache staging artifact
+        uses: actions/download-artifact@37930b1c2abaa49bbe596cd826c3c89aef350131 # v7.0.0
+        with:
+          name: cache-staging
+          path: cache-staging
+
+      - name: Upload staged cache to Azure
+        shell: bash
+        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:]]}"}"
+
+          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
-    needs: [build]
+    needs: [build, upload_cache]
+    if: ${{ always() && needs.build.result == 'success' && (needs.upload_cache.result == 'success' || needs.upload_cache.result == 'skipped') }}
     runs-on: ubuntu-latest # Note these steps run on disposable GitHub runners, so no landrun sandboxing is needed.
     steps:
 
@@ -674,6 +727,7 @@ jobs:
 
       # We no longer run `lean4checker` in regular CI, as it is quite expensive for little benefit.
       # Instead we run it in a cron job on master: see `daily.yml`.
+
   style_lint:
     name: Lint style
     runs-on: ubuntu-latest
@@ -686,7 +740,8 @@ jobs:
 
   final:
     name: Post-CI job
-    if: ${{ inputs.run_post_ci }}
+    # ensure that this runs iff direct dependencies succeeded even if transitive dependencies  were skipped
+    if: ${{ always() && inputs.run_post_ci && needs.style_lint.result == 'success' && needs.build.result == 'success' && needs.post_steps.result == 'success' }}
     needs: [style_lint, build, post_steps]
     runs-on: ubuntu-latest
     steps:

.github/workflows/commit_verification.yml

@@ -22,7 +22,9 @@ permissions:
 
 env:
   TRANSIENT_PREFIX: "transient: "
-  AUTO_PREFIX: "x: "
+  # Support both "x " and "x: " (legacy) prefixes
+  AUTO_PREFIX_COLON: "x: "
+  AUTO_PREFIX_SPACE: "x "
 
 jobs:
   verify:
@@ -46,8 +48,9 @@ jobs:
           HEAD_SHA="${{ github.event.pull_request.head.sha }}"
 
           # Check if any commits have transient or auto prefix
+          # Auto prefix can be "x " or "x: " (legacy)
           HAS_SPECIAL=$(git log --format="%s" "$BASE_SHA..$HEAD_SHA" | \
-            grep -E "^(${TRANSIENT_PREFIX}|${AUTO_PREFIX})" || true)
+            grep -E "^(${TRANSIENT_PREFIX}|${AUTO_PREFIX_COLON}|${AUTO_PREFIX_SPACE})" || true)
 
           if [[ -n "$HAS_SPECIAL" ]]; then
             echo "has_special=true" >> "$GITHUB_OUTPUT"

.github/workflows/nightly_bump_and_merge.yml

@@ -230,7 +230,7 @@ jobs:
           }
 
           # Find tags that are ancestors of this branch with the right format
-          LATEST_TAG=$(git tag --merged HEAD | grep "nightly-testing-[0-9]\{4\}-[0-9]\{2\}-[0-9]\{2\}" | sort -r | head -n 1)
+          LATEST_TAG=$(git tag --merged HEAD | grep "nightly-testing-[0-9]\{4\}-[0-9]\{2\}-[0-9]\{2\}\(-rev[0-9]\+\)\?" | sort -rV | head -n 1)
           echo "Latest tag found for $BRANCH: ${LATEST_TAG:-none}"
 
           # Return to nightly-testing branch

.github/workflows/nightly_detect_failure.yml

@@ -274,7 +274,7 @@ jobs:
           core.setOutput('toolchain_content', content);
           core.setOutput('branch_name', branchName);
 
-          const match = content.match(/leanprover\/lean4:nightly-(\d{4}-\d{2}-\d{2})/);
+          const match = content.match(/leanprover\/lean4:nightly-(\d{4}-\d{2}-\d{2}(?:-rev\d+)?)/);
           if (!match) {
             core.setFailed('Toolchain pattern did not match');
             return null;
@@ -292,7 +292,7 @@ jobs:
         type: 'stream'
         topic: 'Mathlib status updates'
         content: |
-          ⚠️ Warning: The lean-toolchain file in bump branch `${{ steps.bump_version.outputs.branch_name }}` does not match the expected pattern 'leanprover/lean4:nightly-YYYY-MM-DD'.
+          ⚠️ Warning: The lean-toolchain file in bump branch `${{ steps.bump_version.outputs.branch_name }}` does not match the expected pattern 'leanprover/lean4:nightly-YYYY-MM-DD(-revK)'.
 
           **Branch:** `${{ steps.bump_version.outputs.branch_name }}`
           **File URL:** https://github.com/${{ github.repository }}/blob/${{ steps.bump_version.outputs.branch_sha }}/lean-toolchain
@@ -418,7 +418,7 @@ jobs:
             if last_bot_message:
                 last_content = last_bot_message['content']
                 # Extract nightly date and bump branch from last bot message
-                date_match = re.search(r'bump/nightly-(\d{4}-\d{2}-\d{2})', last_content)
+                date_match = re.search(r'bump/nightly-(\d{4}-\d{2}-\d{2}(?:-rev\d+)?)', last_content)
                 branch_match = re.search(r'PR that to (bump/v[\d.]+)', last_content)
                 if date_match and branch_match:
                     last_date = date_match.group(1)

.github/workflows/nolints.yml

@@ -36,6 +36,8 @@ jobs:
       - name: Create Pull Request
         uses: peter-evans/create-pull-request@c0f553fe549906ede9cf27b5156039d195d2ece0 # v8.1.0
         with:
+          # this needs to be set, otherwise the last person who edited the `cron` line may get tagged
+          author: "mathlib-nolints[bot] <258989889+mathlib-nolints[bot]@users.noreply.github.com>"
           token: ${{ steps.app-token.outputs.token }}
           commit-message: "chore(scripts): update nolints.json"
           branch: "nolints"
@@ -44,5 +46,7 @@ jobs:
           body: |
             I am happy to remove some nolints for you!
 
+            ---
+
             [workflow run for this PR](${{ github.server_url }}/${{ github.repository }}/actions/runs/${{ github.run_id }})
           labels: "auto-merge-after-CI"

.github/workflows/remove_deprecated_decls.yml

@@ -218,6 +218,8 @@ jobs:
       if: ${{ steps.process_dates.outputs.from_date && toJson(inputs.dry_run) != 'true' && steps.find-pr.outputs.pr_found != 'true' }}
       uses: peter-evans/create-pull-request@c0f553fe549906ede9cf27b5156039d195d2ece0 # v8.1.0
       with:
+        # this needs to be set, otherwise the last person who edited the `cron` line may get tagged
+        author: "mathlib-nolints[bot] <258989889+mathlib-nolints[bot]@users.noreply.github.com>"
         token: ${{ steps.app-token.outputs.token }}
         commit-message: "chore: remove declarations deprecated between ${{ steps.process_dates.outputs.from_date }} and ${{ steps.process_dates.outputs.to_date }}"
         branch: ${{ env.BRANCH_NAME }}

.github/workflows/update_dependencies.yml

@@ -124,6 +124,8 @@ jobs:
         if: ${{ steps.pr-title.outcome == 'success' }}
         uses: peter-evans/create-pull-request@c0f553fe549906ede9cf27b5156039d195d2ece0 # v8.1.0
         with:
+          # this needs to be set, otherwise the last person who edited the `cron` line may get tagged
+          author: "mathlib-update-dependencies[bot] <258990618+mathlib-update-dependencies[bot]@users.noreply.github.com>"
           token: ${{ steps.app-token.outputs.token }}
           commit-message: "chore: update Mathlib dependencies ${{ env.timestamp }}"
           # this branch is referenced in update_dependencies_zulip.yml

.github/workflows/zulip_emoji_ci_status.yaml

@@ -0,0 +1,101 @@
+name: Zulip emoji CI status
+
+on:
+  workflow_run:
+    workflows: ["continuous integration", "continuous integration (mathlib forks)"]
+    types: [requested, completed]
+
+# Limit permissions for GITHUB_TOKEN for the entire workflow
+permissions:
+  contents: read
+  pull-requests: read
+  # All other permissions are implicitly 'none'
+
+jobs:
+  update_ci_emoji:
+    runs-on: ubuntu-latest
+    if: github.repository == 'leanprover-community/mathlib4'
+    steps:
+    - name: Determine PR number
+      id: pr
+      env:
+        GH_TOKEN: ${{ github.token }}
+        HEAD_BRANCH: ${{ github.event.workflow_run.head_branch }}
+        HEAD_REPO_OWNER: ${{ github.event.workflow_run.head_repository.owner.login }}
+        HEAD_SHA: ${{ github.event.workflow_run.head_sha }}
+      run: |
+        # Try to get PR number from the workflow_run event
+        PR_NUMBER=$(echo '${{ toJSON(github.event.workflow_run.pull_requests) }}' | jq -r '.[0].number // empty')
+        # For push-triggered CI (non-fork PRs), pull_requests may be empty;
+        # fall back to looking up the PR by branch name.
+        # Use owner:branch format to avoid matching the wrong PR when
+        # multiple forks use the same branch name.
+        if [ -z "$PR_NUMBER" ]; then
+          PR_NUMBER=$(gh pr list --repo "${{ github.repository }}" --head "$HEAD_REPO_OWNER:$HEAD_BRANCH" --state open --json number,headRefOid --jq ".[] | select(.headRefOid == \"$HEAD_SHA\") | .number" 2>/dev/null || true)
+        fi
+        # If owner-qualified lookup failed, try without owner (for same-repo branches)
+        if [ -z "$PR_NUMBER" ]; then
+          PR_NUMBER=$(gh pr list --repo "${{ github.repository }}" --head "$HEAD_BRANCH" --state open --json number,headRefOid --jq ".[] | select(.headRefOid == \"$HEAD_SHA\") | .number" 2>/dev/null || true)
+        fi
+        if [ -z "$PR_NUMBER" ]; then
+          echo "No PR found for branch $HEAD_REPO_OWNER:$HEAD_BRANCH at $HEAD_SHA, skipping"
+          echo "skip=true" >> "$GITHUB_OUTPUT"
+        else
+          echo "Found PR #$PR_NUMBER"
+          echo "pr_number=$PR_NUMBER" >> "$GITHUB_OUTPUT"
+          echo "skip=false" >> "$GITHUB_OUTPUT"
+        fi
+
+    - name: Determine CI action
+      id: action
+      if: steps.pr.outputs.skip != 'true'
+      run: |
+        EVENT_ACTION="${{ github.event.action }}"
+        CONCLUSION="${{ github.event.workflow_run.conclusion }}"
+        echo "Event action: $EVENT_ACTION, conclusion: $CONCLUSION"
+        if [ "$EVENT_ACTION" = "requested" ]; then
+          echo "ci_action=ci-running" >> "$GITHUB_OUTPUT"
+        elif [ "$EVENT_ACTION" = "completed" ]; then
+          case "$CONCLUSION" in
+            success)
+              echo "ci_action=ci-success" >> "$GITHUB_OUTPUT"
+              ;;
+            cancelled)
+              # Clear the running emoji. A new run may or may not follow
+              # (manual cancel, branch deleted, etc.), so don't leave stale 🟡.
+              echo "ci_action=ci-cancelled" >> "$GITHUB_OUTPUT"
+              ;;
+            *)
+              echo "ci_action=ci-failure" >> "$GITHUB_OUTPUT"
+              ;;
+          esac
+        fi
+
+    - name: Checkout mathlib repository
+      if: steps.pr.outputs.skip != 'true' && steps.action.outputs.ci_action != 'skip'
+      uses: actions/checkout@de0fac2e4500dabe0009e67214ff5f5447ce83dd # v6.0.2
+      with:
+        ref: master
+        sparse-checkout: |
+          scripts/zulip_emoji_reactions.py
+
+    - name: Set up Python
+      if: steps.pr.outputs.skip != 'true' && steps.action.outputs.ci_action != 'skip'
+      uses: actions/setup-python@a309ff8b426b58ec0e2a45f0f869d46889d02405 # v6.2.0
+      with:
+        python-version: '3.x'
+
+    - name: Install dependencies
+      if: steps.pr.outputs.skip != 'true' && steps.action.outputs.ci_action != 'skip'
+      run: |
+        python -m pip install --upgrade pip
+        pip install zulip
+
+    - name: Update CI emoji
+      if: steps.pr.outputs.skip != 'true' && steps.action.outputs.ci_action != 'skip'
+      env:
+        ZULIP_API_KEY: ${{ secrets.ZULIP_API_KEY }}
+        ZULIP_EMAIL: github-mathlib4-bot@leanprover.zulipchat.com
+        ZULIP_SITE: https://leanprover.zulipchat.com
+      run: |
+        python scripts/zulip_emoji_reactions.py "$ZULIP_API_KEY" "$ZULIP_EMAIL" "$ZULIP_SITE" "${{ steps.action.outputs.ci_action }}" "none" "${{ steps.pr.outputs.pr_number }}"

Archive/Examples/Eisenstein.lean

@@ -25,6 +25,7 @@ namespace Polynomial
 
 open Ideal.Quotient Ideal RingHom
 
+set_option backward.isDefEq.respectTransparency false in
 set_option linter.flexible false in
 example : Irreducible (X ^ 4 - 10 * X ^ 2 + 1 : ℤ[X]) := by
   -- We will apply the generalized Eisenstein criterion with `q = X ^ 2 + 1` and `K = ZMod 3`.