Merge branch 'master' into codex/add-inline-comment-for-heartbeat-count

Author: kim-em

.github/PULL_REQUEST_TEMPLATE.md

@@ -11,10 +11,13 @@ In particular, note that most reviewers will only notice your PR
 if it passes the continuous integration checks.
 Please ask for help on https://leanprover.zulipchat.com if needed.
 
-To indicate co-authors, include lines at the bottom of the commit message
-(that is, before the `---`) using the following format:
+To indicate co-authors, include at least one commit authored by each
+co-author among the commits in the pull request. If necessary, you may 
+create empty commits to indicate co-authorship, using commands like so:
+
+git commit --author="Author Name <author@email.com>" --allow-empty -m "add Author Name as coauthor"
 
-Co-authored-by: Author Name <author@email.com>
+When merging, all the commits will be squashed into a single commit listing all co-authors.
 
 If you are moving or deleting declarations, please include these lines at the bottom of the commit message
 (that is, before the `---`) using the following format:

.github/build.in.yml

@@ -43,12 +43,16 @@ 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 -- bash -euxo pipefail {0}
     steps:
       - name: cleanup
         shell: bash    # This *just* deletes old files, so is safe to run outside landrun.
         run: |
-          find . -name . -o -prune -exec rm -rf -- {} +
+          if ! find . -mindepth 1 -exec rm -rf -- {} +; then
+            echo "ERROR: Initial cleanup failed, waiting 5 seconds and retrying..."
+            sleep 5
+            find . -mindepth 1 -exec rm -rf -- {} +
+          fi
           # Delete all but the 5 most recent toolchains.
           # Make sure to delete both the `~/.elan/toolchains/X` directory and the `~/.elan/update-hashes/X` file.
           # Skip symbolic links (`-type d`), the current directory (`! -name .`), and `nightly` and `stable`.
@@ -66,7 +70,10 @@ jobs:
       - name: Checkout master branch
         uses: actions/checkout@11bd71901bbe5b1630ceea73d27597364c9af683 # v4.2.2
         with:
-          ref: master
+          # Recall that on the `leanprover-community/mathlib4-nightly-testing` repository,
+          # we don't maintain a `master` branch at all.
+          # For PRs and pushes to this repository, we will use `nightly-testing` instead.
+          ref: ${{ github.repository == 'leanprover-community/mathlib4-nightly-testing' && 'nightly-testing' || 'master' }}
           path: master-branch
 
       # Checkout the PR branch into a subdirectory
@@ -198,8 +205,8 @@ jobs:
         run: |
           cd pr-branch
 
-          echo "Attempting: lake build --no-build Mathlib.Init (this runs under landrun)"
-          lake build --no-build Mathlib.Init
+          echo "Attempting: lake build --no-build -v Mathlib.Init (this runs under landrun)"
+          lake build --no-build -v Mathlib.Init
 
       - name: get cache (3/3 - finalize cache operation)
         id: get
@@ -210,8 +217,11 @@ jobs:
             echo "Fetching all remaining cache..."
 
             ../master-branch/.lake/build/bin/cache get
+
+            # Run again with --repo, to ensure we actually get the oleans.
+            ../master-branch/.lake/build/bin/cache --repo=${{ github.event.pull_request.head.repo.full_name || github.repository }} get
           else
-            echo "WARNING: 'lake build --no-build Mathlib.Init' failed."
+            echo "WARNING: 'lake build --no-build -v Mathlib.Init' failed."
             echo "No cache for 'Mathlib.Init' available or it could not be prepared."
           fi
 
@@ -233,14 +243,17 @@ jobs:
         id: build
         run: |
           cd pr-branch
+          echo "::group::{test curl}"
           # Test curl - should fail when landrun network isolation is working
           if curl --silent --head --fail https://www.example.com/ >/dev/null 2>&1; then
             echo "ERROR: curl to example.com succeeded, but it should fail when landrun is working correctly!"
             exit 1
           else
             echo "curl to example.com failed as expected - landrun network isolation is working"
           fi
-          bash -o pipefail -c "env LEAN_ABORT_ON_PANIC=1 lake build --wfail -KCI"
+          echo "::endgroup::"
+
+          ../master-branch/scripts/lake-build-with-retry.sh Mathlib
       - name: end gh-problem-match-wrap for build step
         uses: leanprover-community/gh-problem-matcher-wrap@20007cb926a46aa324653a387363b52f07709845 # 2025-04-23
         with:
@@ -252,6 +265,17 @@ jobs:
           cd pr-branch
           du .lake/build/lib/lean/Mathlib || echo "This code should be unreachable"
 
+      - name: upload artifact containing contents of pr-branch
+        # temporary measure for debugging no-build failures
+        uses: actions/upload-artifact@ea165f8d65b6e75b540449e92b4886f43607fa02 # v4.6.2
+        with:
+          name: mathlib4_artifact
+          include-hidden-files: true
+          # we exclude .git since there may be secrets in there
+          path: |
+            pr-branch/
+            !pr-branch/.git/
+
       # The cache secrets are available here, so we must not run any untrusted code.
       - name: upload cache
         # We only upload the cache if the build started (whether succeeding, failing, or cancelled)
@@ -262,36 +286,20 @@ jobs:
         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:]]}"}"
+
           # 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 put-unpacked
+          ../master-branch/.lake/build/bin/cache --repo=${{ github.event.pull_request.head.repo.full_name || github.repository }} put-unpacked
         env:
-          MATHLIB_CACHE_SAS: ${{ secrets.MATHLIB_CACHE_SAS }}
-          MATHLIB_CACHE_S3_TOKEN: ${{ secrets.MATHLIB_CACHE_S3_TOKEN }}
-
-      - name: check the cache
-        # We need network access to download dependencies
-        # We run this inside landrun, but restrict disk access as usual.
-        shell: landrun --unrestricted-network --rox /usr --rw /dev --rox /etc --rox /home/lean/.elan --rox /home/lean/actions-runner/_work --rox /home/lean/.cache/mathlib -rw pr-branch/.lake/ --rw pr-branch/DownstreamTest/ --env PATH --env HOME --env GITHUB_OUTPUT -- bash -euxo pipefail {0}
-        run: |
-          cd pr-branch
-
-          # Because the `lean-pr-testing-NNNN` branches use toolchains that are "updated in place"
-          # the cache mechanism is unreliable, so we don't test it if we are on such a branch.
-          if [[ ! $(cat lean-toolchain) =~ ^leanprover/lean4-pr-releases:pr-release-[0-9]+$ ]]; then
-            cd DownstreamTest
-            MATHLIB_NO_CACHE_ON_UPDATE=1 lake update
-
-            lake env ../../master-branch/.lake/build/bin/cache get || (sleep 1; lake env ../../master-branch/.lake/build/bin/cache get)
-
-            # We need to run `lake build ProofWidgets` here to retrieve ProofWidgets via Reservoir.
-            lake build ProofWidgets
-            lake build --no-build Mathlib
-          fi
+          MATHLIB_CACHE_SAS_RAW: ${{ secrets.MATHLIB_CACHE_SAS }}
+          MATHLIB_CACHE_S3_TOKEN_RAW: ${{ secrets.MATHLIB_CACHE_S3_TOKEN }}
 
       # 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
@@ -310,26 +318,44 @@ jobs:
 
       - name: build archive
         id: archive
+        continue-on-error: true
         run: |
           cd pr-branch
-          bash -o pipefail -c "env LEAN_ABORT_ON_PANIC=1 lake build Archive"
+          ../master-branch/scripts/lake-build-with-retry.sh Archive
 
       - name: build counterexamples
         id: counterexamples
+        continue-on-error: true
         run: |
           cd pr-branch
-          bash -o pipefail -c "env LEAN_ABORT_ON_PANIC=1 lake build Counterexamples"
+          ../master-branch/scripts/lake-build-with-retry.sh Counterexamples
+
+      - name: Check if building Archive or Counterexamples failed
+        if: steps.archive.outcome == 'failure' || steps.counterexamples.outcome == 'failure'
+        run: |
+          if [ "${{ steps.archive.outcome }}" == "failure" ]; then
+            echo "❌ The \"build archive\" step above failed; please check its logs."
+          fi
+          if [ "${{ steps.counterexamples.outcome }}" == "failure" ]; then
+            echo "❌ The \"build counterexamples\" step above failed; please check its logs."
+          fi
+          exit 1
 
       # The cache secrets are available here, so we must not run any untrusted code.
       - name: put archive and counterexamples cache
         shell: bash
         run: |
           cd pr-branch
-          ../master-branch/.lake/build/bin/cache put Archive.lean
-          ../master-branch/.lake/build/bin/cache put Counterexamples.lean
+
+          # 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
         env:
-          MATHLIB_CACHE_SAS: ${{ secrets.MATHLIB_CACHE_SAS }}
-          MATHLIB_CACHE_S3_TOKEN: ${{ secrets.MATHLIB_CACHE_S3_TOKEN }}
+          MATHLIB_CACHE_SAS_RAW: ${{ secrets.MATHLIB_CACHE_SAS }}
+          MATHLIB_CACHE_S3_TOKEN_RAW: ${{ secrets.MATHLIB_CACHE_S3_TOKEN }}
 
       - name: Check {Mathlib, Tactic, Counterexamples, Archive}.lean
         if: always()
@@ -393,7 +419,7 @@ jobs:
             ##  we filter out the output lines that begin with `✔ [xx/yy]`, where xx, yy
             ##  are either numbers or ?, and the "Build completed successfully." message.
             ##  We keep the rest, which are actual outputs of the files
-            awk '!($0 ~ "^\\s*✔ \\[[?0-9]*/[?0-9]*\\]" || $0 == "Build completed successfully."){ print $0 }')"
+            awk '!($0 ~ "^\\s*✔ \\[[?0-9]*/[?0-9]*\\]" || $0 ~ "^Build completed successfully( \\([0-9]+ jobs\\))?\\.?$"){ print $0 }')"
           if [ -n "${buildMsgs}" ]
           then
             printf $'%s\n' "${buildMsgs}"
@@ -413,6 +439,7 @@ jobs:
           COUNTEREXAMPLES_OUTCOME: ${{ steps.counterexamples.outcome }}
           LINT_OUTCOME: ${{ steps.lint.outcome }}
           TEST_OUTCOME: ${{ steps.test.outcome }}
+          NIGHTLY_TESTING_REPO: leanprover-community/mathlib4-nightly-testing
         run: |
           master-branch/scripts/lean-pr-testing-comments.sh lean
           master-branch/scripts/lean-pr-testing-comments.sh batteries
@@ -425,6 +452,8 @@ jobs:
     steps:
 
       - uses: actions/checkout@11bd71901bbe5b1630ceea73d27597364c9af683 # v4.2.2
+        with:
+          ref: "${{ PR_BRANCH_REF }}"
 
       - name: Configure Lean
         uses: leanprover/lean-action@f807b338d95de7813c5c50d018f1c23c9b93b4ec # 2025-04-24
@@ -434,15 +463,33 @@ jobs:
           use-mathlib-cache: true
           reinstall-transient-toolchain: true
 
+      # TODO: this step should not be necessary, "Configure Lean" above should already achieve this.
+      - 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.
           lake exe cache get Archive Counterexamples
+          # 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 Archive Counterexamples
 
       - name: verify that everything was available in the cache
         run: |
-          lake build --no-build Mathlib
-          lake build --no-build Archive
-          lake build --no-build Counterexamples
+          echo "::group::{verify Mathlib cache}"
+          lake build --no-build -v Mathlib
+          echo "::endgroup::"
+          echo "::group::{verify Archive cache}"
+          lake build --no-build -v Archive
+          echo "::endgroup::"
+          echo "::group::{verify Counterexamples cache}"
+          lake build --no-build -v Counterexamples
+          echo "::endgroup::"
 
       - name: check declarations in db files
         run: |
@@ -504,10 +551,11 @@ jobs:
     if: FORK_CONDITION
     runs-on: ubuntu-latest
     steps:
-      - uses: leanprover-community/lint-style-action@f2e7272aad56233a642b08fe974cf09dd664b0c8 # 2025-05-22
+      - uses: leanprover-community/lint-style-action@d29fb3b12c1c834450680b3c544f63fe0237a2e2 # 2025-06-20
         with:
           mode: check
           lint-bib-file: true
+          ref: ${{ PR_BRANCH_REF }}
 
   build_and_lint:
     name: CI Success

.github/workflows/PR_summary.yml

@@ -13,6 +13,7 @@ jobs:
   build:
     name: "post-or-update-summary-comment"
     runs-on: ubuntu-latest
+    if: github.repository == 'leanprover-community/mathlib4'
 
     steps:
     - name: Checkout code

.github/workflows/auto_assign_reviewers.yaml

@@ -0,0 +1,29 @@
+name: automatically assign reviewers
+
+on:
+  schedule:
+    - cron: "37 0 * * *" # At 00:37 UTC every day
+  workflow_dispatch:
+
+jobs:
+  autoassign-reviewers:
+    if: github.repository == 'leanprover-community/mathlib4'
+    name: assign automatically proposed reviewers
+    runs-on: ubuntu-latest
+    steps:
+      - uses: actions/checkout@11bd71901bbe5b1630ceea73d27597364c9af683 # v4.2.2
+        with:
+          ref: master
+          sparse-checkout: |
+            scripts/assign_reviewers.py
+
+      - name: Set up Python
+        uses: actions/setup-python@a26af69be951a213d495a4c3e4e4022e16d87065 # v5.6.0
+        with:
+          python-version: '3.x'
+
+      - name: assign reviewers
+        env:
+          ASSIGN_REVIEWERS_TOKEN: ${{ secrets.ASSIGN_REVIEWERS }}
+        run: |
+          python3 scripts/assign_reviewers.py