Merge remote-tracking branch 'origin/master' into CB_Eisenstein_E2

Author: CBirkbeck

.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

@@ -48,7 +48,11 @@ jobs:
       - 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
@@ -268,31 +275,11 @@ jobs:
           # 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
-
       # 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.
@@ -325,8 +312,8 @@ jobs:
         shell: bash
         run: |
           cd pr-branch
-          ../master-branch/.lake/build/bin/cache put Archive.lean
-          ../master-branch/.lake/build/bin/cache put Counterexamples.lean
+          ../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 }}
@@ -413,6 +400,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 +413,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,9 +424,21 @@ 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: |
@@ -504,10 +506,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
@@ -538,11 +541,13 @@ jobs:
           filterOutClosed: true
 
       # 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!
       - id: PR
         shell: bash
         run: |
-          echo "number=${{ steps.PR_from_push.outputs.number || github.event.pull_request.number }}" >> $GITHUB_OUTPUT
-          echo "pr_labels=${{ steps.PR_from_push.outputs.pr_labels || join(github.event.pull_request.labels.*.name, ',') }}" >> $GITHUB_OUTPUT
+          echo "number=${{ steps.PR_from_push.outputs.number || github.event.pull_request.number }}" | tee -a "$GITHUB_OUTPUT"
+          echo "pr_labels=${{ steps.PR_from_push.outputs.pr_labels || join(github.event.pull_request.labels.*.name, ',') }}" | tee -a "$GITHUB_OUTPUT"
 
       - if: contains(steps.PR.outputs.pr_labels, 'bench-after-CI')
         name: If `bench-after-CI` is present, add a `!bench` comment.
@@ -563,6 +568,74 @@ jobs:
             --header 'authorization: Bearer ${{ secrets.GITHUB_TOKEN }}'
 
       - if: contains(steps.PR.outputs.pr_labels, 'auto-merge-after-CI')
+        name: Get PR label timeline data
+        # 'auto-merge-after-CI' must be within the last 100 labels added (could be increased to 250 if needed)
+        # query from https://stackoverflow.com/a/67939355
+        # unfortunately we cannot query only for 'auto-merge-after-CI' events
+        # so we have to process this with jq in the next step
+        id: get-timeline
+        uses: octokit/graphql-action@8ad880e4d437783ea2ab17010324de1075228110 # v2.3.2
+        with:
+          query: |
+            query($owner: String!, $name: String!, $number: Int!) {
+              repository(owner: $owner, name: $name) {
+                pullRequest(number: $number) {
+                  timelineItems(itemTypes: LABELED_EVENT, last: 100) {
+                    nodes {
+                      ... on LabeledEvent {
+                        createdAt
+                        actor { login }
+                        label { name }
+                      }
+                    }
+                  }
+                }
+              }
+            }
+          owner: leanprover-community
+          name: mathlib4
+          number: ${{ steps.PR.outputs.number }}
+        env:
+          GITHUB_TOKEN: ${{ secrets.GITHUB_TOKEN }}
+
+      - if: contains(steps.PR.outputs.pr_labels, 'auto-merge-after-CI')
+        name: Extract label actor username
+        id: get-label-actor
+        run: |
+          # Parse the GraphQL response and filter for the specific label
+          echo '${{ steps.get-timeline.outputs.data }}'
+          USERNAME=$(echo '${{ steps.get-timeline.outputs.data }}' | jq -r '
+            .repository.pullRequest.timelineItems.nodes
+            | map(select(.label.name == "auto-merge-after-CI"))
+            | sort_by(.createdAt)
+            | last
+            | .actor.login // empty
+          ')
+
+          # Validate username format (GitHub usernames are alphanumeric + hyphens, max 39 chars)
+          printf 'USERNAME: %s\n' "$USERNAME"
+          if [[ -z "$USERNAME" ]]; then
+            echo "Error: No actor found for the specified label"
+            exit 1
+          elif ! [[ "$USERNAME" =~ ^[a-zA-Z0-9-]{1,39}$ ]]; then
+            echo "Error: Invalid username format: $USERNAME"
+            exit 1
+          fi
+
+          echo "username=$USERNAME" >> "$GITHUB_OUTPUT"
+          echo "Found label actor: $USERNAME"
+
+      - if: contains(steps.PR.outputs.pr_labels, 'auto-merge-after-CI')
+        name: check team membership
+        uses: tspascoal/get-user-teams-membership@57e9f42acd78f4d0f496b3be4368fc5f62696662 # v3.0.0
+        id: actorTeams
+        with:
+          organization: leanprover-community # optional. Default value ${{ github.repository_owner }}
+                  # Organization to get membership from.
+          username: ${{ steps.get-label-actor.outputs.username }}
+          GITHUB_TOKEN: ${{ secrets.MATHLIB_REVIEWERS_TEAM_KEY }} # (Requires scope: `read:org`)
+
+      - if: ${{ contains(steps.PR.outputs.pr_labels, 'auto-merge-after-CI') && (contains(steps.actorTeams.outputs.teams, 'mathlib-maintainers') || contains(steps.actorTeams.outputs.teams, 'bot-users')) }}
         name: If `auto-merge-after-CI` is present, add a `bors merge` comment.
         uses: GrantBirki/comment@608e41b19bc973020ec0e189ebfdae935d7fe0cc # v2.1.1
         with:

.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