Merge remote-tracking branch 'upstream/master' into batteries-pr-testing-1589

Author: fgdorais

.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,52 @@ jobs:
           ../tools-branch/scripts/lake-build-with-retry.sh Counterexamples
           # results of build at pr-branch/.lake/build_summary_Counterexamples.json
 
+      - name: prepare cache staging directory
+        if: ${{ steps.build.outcome == 'success' }}
+        shell: bash
+        run: |
+          rm -rf cache-staging
+          mkdir -p cache-staging
+
+      - name: stage Mathlib cache files
+        if: ${{ steps.build.outcome == 'success' }}
+        shell: bash
+        run: |
+          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: ${{ steps.build.outcome == 'success' }}
+        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: ${{ 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 +456,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 +602,59 @@ 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.build-outcome == 'success' && needs.build.outputs.get-cache-outcome == 'success' && 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]
     runs-on: ubuntu-latest # Note these steps run on disposable GitHub runners, so no landrun sandboxing is needed.
     steps:
 
@@ -674,6 +731,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

.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