Merge branch 'master' into one_sub-results

Author: mitchell-horner

.github/actionlint.yml

@@ -2,3 +2,4 @@ self-hosted-runner:
   labels:
     - bors
     - pr
+    - doc-gen

.github/build.in.yml

@@ -43,7 +43,7 @@ jobs:
       test-outcome: ${{ steps.test.outcome }}
     defaults: # On Hoskinson runners, landrun is already installed.
       run:
-        shell: landrun --rox /usr --rw /dev --rox /home/lean/.elan --rox /home/lean/actions-runner/_work --rox /home/lean/.cache/mathlib/ --rw pr-branch/.lake/ --env PATH --env HOME --env GITHUB_OUTPUT -- bash -euxo pipefail {0}
+        shell: landrun --rox /usr --ro /etc/timezone --rw /dev --rox /home/lean/.elan --rox /home/lean/actions-runner/_work --rox /home/lean/.cache/mathlib/ --rw pr-branch/.lake/ --env PATH --env HOME --env GITHUB_OUTPUT --env CI -- bash -euxo pipefail {0}
     steps:
       - name: cleanup
         shell: bash    # This *just* deletes old files, so is safe to run outside landrun.
@@ -181,11 +181,38 @@ jobs:
         # - we give --rox access to `~/.elan` and `~/actions-runner/_work` (GitHub CI needs this)
         # - we give --unrestricted-network as we need this to download dependencies
         # - git needs read only access to `/etc`.
-        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 -- bash -euxo pipefail {0}
+        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 env
 
+      - name: validate lake-manifest.json inputRevs
+        # Only enforce this on the main mathlib4 repository, not on nightly-testing
+        if: github.repository == 'leanprover-community/mathlib4'
+        shell: bash
+        run: |
+          cd pr-branch
+
+          # Check that all inputRevs in lake-manifest.json match the required pattern
+          echo "Validating lake-manifest.json inputRevs..."
+
+          # Extract all inputRevs from the manifest
+          invalid_revs=$(jq -r '.packages[].inputRev // empty' lake-manifest.json | \
+            grep -v -E '^(main|master|v[0-9]+\.[0-9]+\.[0-9]+(-[a-zA-Z0-9.-]+)?)$' || true)
+
+          if [ -n "$invalid_revs" ]; then
+            echo "❌ Error: Found invalid inputRevs in lake-manifest.json:"
+            echo "$invalid_revs"
+            echo ""
+            echo "All inputRevs must be one of:"
+            echo "  - 'main'"
+            echo "  - 'master'"
+            echo "  - 'vX.Y.Z' (semantic version, e.g., v1.2.3 or v1.2.3-pre)"
+            exit 1
+          else
+            echo "✅ All inputRevs in lake-manifest.json are valid"
+          fi
+
       - name: get cache (1/3 - setup and initial fetch)
         id: get_cache_part1_setup
         shell: bash # only runs `cache get` from `master-branch`, so doesn't need to be inside landrun
@@ -277,7 +304,7 @@ jobs:
             !pr-branch/.git/
 
       # The cache secrets are available here, so we must not run any untrusted code.
-      - name: upload cache
+      - 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
@@ -288,19 +315,50 @@ jobs:
 
           # 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:]]}"}"
-          export MATHLIB_CACHE_S3_TOKEN="${MATHLIB_CACHE_S3_TOKEN_RAW%"${MATHLIB_CACHE_S3_TOKEN_RAW##*[![:space:]]}"}"
 
           # Use the trusted cache tool from master-branch
           # TODO: this is not doing anything currently, and needs to be integrated with put-unpacked
           # ../master-branch/.lake/build/bin/cache commit || true
           # run this in CI if it gets an incorrect lake hash for existing cache files somehow
           # ../master-branch/.lake/build/bin/cache put!
           # do not try to upload files just downloaded
-          ../master-branch/.lake/build/bin/cache --repo=${{ github.event.pull_request.head.repo.full_name || github.repository }} put-unpacked
+
+          echo "Uploading cache to Azure..."
+          USE_FRO_CACHE=0 ../master-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 }}
+
+      # The cache secrets are available here, so we must not run any untrusted code.
+      - name: Upload cache to Cloudflare
+        id: cloudflare-upload-mathlib
+        if: ${{ always() && steps.get.outcome == 'success' }}
+        continue-on-error: true
+        shell: bash
+        run: |
+          cd pr-branch
+
+          # Trim trailing whitespace from secrets to prevent issues with accidentally added spaces
+          export MATHLIB_CACHE_S3_TOKEN="${MATHLIB_CACHE_S3_TOKEN_RAW%"${MATHLIB_CACHE_S3_TOKEN_RAW##*[![:space:]]}"}"
+
+          echo "Uploading cache to Cloudflare..."
+          USE_FRO_CACHE=1 ../master-branch/.lake/build/bin/cache --repo=${{ github.event.pull_request.head.repo.full_name || github.repository }} put-unpacked
+        env:
           MATHLIB_CACHE_S3_TOKEN_RAW: ${{ secrets.MATHLIB_CACHE_S3_TOKEN }}
 
+      - name: Report Cloudflare upload failure on Zulip
+        if: steps.cloudflare-upload-mathlib.outcome == 'failure'
+        uses: zulip/github-actions-zulip/send-message@e4c8f27c732ba9bd98ac6be0583096dea82feea5 # v1.0.2
+        with:
+          api-key: ${{ secrets.ZULIP_API_KEY }}
+          email: 'github-mathlib4-bot@leanprover.zulipchat.com'
+          organization-url: 'https://leanprover.zulipchat.com'
+          to: 'nightly-testing'
+          type: 'stream'
+          topic: 'Cloudflare cache upload failure'
+          content: |
+            ❌ Cloudflare cache upload (Mathlib) [failed](https://github.com/${{ github.repository }}/actions/runs/${{ github.run_id }}) for PR #${{ github.event.pull_request.number || 'push' }} on commit ${{ github.sha }}
+        continue-on-error: true
+
       # 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.
@@ -342,21 +400,50 @@ jobs:
           exit 1
 
       # The cache secrets are available here, so we must not run any untrusted code.
-      - name: put archive and counterexamples cache
+      - 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:]]}"}"
-          export MATHLIB_CACHE_S3_TOKEN="${MATHLIB_CACHE_S3_TOKEN_RAW%"${MATHLIB_CACHE_S3_TOKEN_RAW##*[![:space:]]}"}"
 
-          ../master-branch/.lake/build/bin/cache --repo=${{ github.event.pull_request.head.repo.full_name || github.repository }} put Archive.lean
-          ../master-branch/.lake/build/bin/cache --repo=${{ github.event.pull_request.head.repo.full_name || github.repository }} put Counterexamples.lean
+          echo "Uploading Archive and Counterexamples cache to Azure..."
+          USE_FRO_CACHE=0 ../master-branch/.lake/build/bin/cache --repo=${{ github.event.pull_request.head.repo.full_name || github.repository }} put Archive.lean
+          USE_FRO_CACHE=0 ../master-branch/.lake/build/bin/cache --repo=${{ github.event.pull_request.head.repo.full_name || github.repository }} put Counterexamples.lean
         env:
           MATHLIB_CACHE_SAS_RAW: ${{ secrets.MATHLIB_CACHE_SAS }}
+
+      - name: Upload Archive and Counterexamples cache to Cloudflare
+        id: cloudflare-upload-archive
+        continue-on-error: true
+        shell: bash
+        run: |
+          cd pr-branch
+
+          # Trim trailing whitespace from secrets to prevent issues with accidentally added spaces
+          export MATHLIB_CACHE_S3_TOKEN="${MATHLIB_CACHE_S3_TOKEN_RAW%"${MATHLIB_CACHE_S3_TOKEN_RAW##*[![:space:]]}"}"
+
+          echo "Uploading Archive and Counterexamples cache to Cloudflare..."
+          USE_FRO_CACHE=1 ../master-branch/.lake/build/bin/cache --repo=${{ github.event.pull_request.head.repo.full_name || github.repository }} put Archive.lean
+          USE_FRO_CACHE=1 ../master-branch/.lake/build/bin/cache --repo=${{ github.event.pull_request.head.repo.full_name || github.repository }} put Counterexamples.lean
+        env:
           MATHLIB_CACHE_S3_TOKEN_RAW: ${{ secrets.MATHLIB_CACHE_S3_TOKEN }}
 
+      - name: Report Cloudflare Archive/Counterexamples upload failure on Zulip
+        if: steps.cloudflare-upload-archive.outcome == 'failure'
+        uses: zulip/github-actions-zulip/send-message@e4c8f27c732ba9bd98ac6be0583096dea82feea5 # v1.0.2
+        with:
+          api-key: ${{ secrets.ZULIP_API_KEY }}
+          email: 'github-mathlib4-bot@leanprover.zulipchat.com'
+          organization-url: 'https://leanprover.zulipchat.com'
+          to: 'nightly-testing'
+          type: 'stream'
+          topic: 'Cloudflare cache upload failure'
+          content: |
+            ❌ Cloudflare cache upload (Archive/Counterexamples) [failed](https://github.com/${{ github.repository }}/actions/runs/${{ github.run_id }}) for PR #${{ github.event.pull_request.number || 'push' }} on commit ${{ github.sha }}
+        continue-on-error: true
+
       - name: Check {Mathlib, Tactic, Counterexamples, Archive}.lean
         if: always()
         run: |
@@ -460,18 +547,39 @@ jobs:
         with:
           auto-config: false # Don't run `lake build`, `lake test`, or `lake lint` automatically.
           use-github-cache: false
-          use-mathlib-cache: true
+          use-mathlib-cache: false # This can be re-enabled once we are confident in the cache again.
           reinstall-transient-toolchain: true
 
-      # TODO: this step should not be necessary, "Configure Lean" above should already achieve this.
+      - name: retrieve and test the Cloudflare caches, but don't fail, just report to Zulip, if anything goes wrong
+        id: cloudflare-cache
+        continue-on-error: true
+        run: |
+          lake exe cache --repo=${{ github.event.pull_request.head.repo.full_name || github.repository }} get
+          lake build --no-build -v Mathlib
+          lake exe cache --repo=${{ github.event.pull_request.head.repo.full_name || github.repository }} get Archive Counterexamples
+          lake build --no-build -v Archive Counterexamples
+
+      - name: Report Cloudflare cache failure on Zulip
+        if: steps.cloudflare-cache.outcome == 'failure'
+        uses: zulip/github-actions-zulip/send-message@e4c8f27c732ba9bd98ac6be0583096dea82feea5 # v1.0.2
+        with:
+          api-key: ${{ secrets.ZULIP_API_KEY }}
+          email: 'github-mathlib4-bot@leanprover.zulipchat.com'
+          organization-url: 'https://leanprover.zulipchat.com'
+          to: 'nightly-testing'
+          type: 'stream'
+          topic: 'Cloudflare cache failure'
+          content: |
+            ❌ Cloudflare cache retrieval/test [failed](https://github.com/${{ github.repository }}/actions/runs/${{ github.run_id }}) for PR #${{ github.event.pull_request.number || 'push' }} on commit ${{ github.sha }}
+        continue-on-error: true
+
       - name: get cache for Mathlib
         run: |
           # Run once without --repo, so we can diagnose what `lake exe cache get` wants to do by itself.
           lake exe cache get
           # Run again with --repo, so ensure we actually get the oleans.
           lake exe cache --repo=${{ github.event.pull_request.head.repo.full_name || github.repository }} get
 
-
       - name: get cache for Archive and Counterexamples
         run: |
           # Run once without --repo, so we can diagnose what `lake exe cache get` wants to do by itself.
@@ -517,6 +625,12 @@ jobs:
         run: |
           lake build Batteries Qq Aesop ProofWidgets Plausible
 
+      - name: build AesopTest (nightly-testing only)
+        # Only run on the mathlib4-nightly-testing repository
+        if: github.repository == 'leanprover-community/mathlib4-nightly-testing'
+        run: |
+          lake build AesopTest
+
       # 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 `lean4checker.yml`.
       # Output is posted to the zulip topic
@@ -551,7 +665,7 @@ jobs:
     if: FORK_CONDITION
     runs-on: ubuntu-latest
     steps:
-      - uses: leanprover-community/lint-style-action@d29fb3b12c1c834450680b3c544f63fe0237a2e2 # 2025-06-20
+      - uses: leanprover-community/lint-style-action@a7e7428fa44f9635d6eb8e01919d16fd498d387a # 2025-08-18
         with:
           mode: check
           lint-bib-file: true
@@ -573,18 +687,16 @@ jobs:
     needs: [style_lint, build, post_steps]
     runs-on: ubuntu-latest
     steps:
-      # This action is used to determine the PR metadata in the event of a push.
-      # If it is called from a PR from a fork, it will find nothing/irrelevant data.
-      - if: github.event_name != 'pull_request_target'
-        id: PR_from_push
-        uses: 8BitJonny/gh-get-current-pr@08e737c57a3a4eb24cec6487664b243b77eb5e36 # 3.0.0
+      - id: PR_from_push
+        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
         with:
           github-token: ${{ secrets.GITHUB_TOKEN }}
           # 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!

.github/workflows/PR_summary.yml

@@ -86,7 +86,7 @@ jobs:
         git diff --name-only --diff-filter D origin/${{ github.base_ref }}... | tee removed_files.txt
         echo "Checking for renamed files..."
 
-        # Shows the `R`enamed files, in human readable format
+        # Shows the `R`enamed files, in human-readable format
         # The `awk` pipe
         # * extracts into an array the old name as the key and the new name as the value
         # * eventually prints "`oldName` was renamed to `newName`" for each key-value pair.