Update lean-toolchain for leanprover/lean4#8883

Author: leanprover-community-mathlib4-bot

.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/actionlint.yml

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

.github/build.in.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
@@ -85,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.

.github/workflows/PR_summary.yml

@@ -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

.github/workflows/auto_assign_reviewers.yaml

@@ -27,7 +27,7 @@ jobs:
     # && (startsWith(github.event.comment.body, 'bot fix style') || contains(toJSON(github.event.comment.body), '\nbot fix style'))
     runs-on: ubuntu-latest
     steps:
-      - uses: leanprover-community/lint-style-action@f2e7272aad56233a642b08fe974cf09dd664b0c8 # 2025-05-22
+      - uses: leanprover-community/lint-style-action@a7e7428fa44f9635d6eb8e01919d16fd498d387a # 2025-08-18
         with:
           mode: fix
           lint-bib-file: true

.github/workflows/bors.yml

@@ -3,6 +3,10 @@ name: Daily CI Workflow
 # running some expensive CI checks that we don't want to run on every PR.
 # It reports results via Zulip.
 
+# This script requires that the ZULIP_API_KEY secret is available in both
+# `leanprover-community/mathlib4` and `leanprover-community/mathlib4-nightly-testing`
+# repositories.
+
 on:
   schedule:
     - cron: '0 0 * * *'   # Runs at 00:00 UTC every day
@@ -15,7 +19,7 @@ env:
 jobs:
   check-lean4checker:
     runs-on: ubuntu-latest
-    if: github.repository == 'leanprover-community/mathlib4'
+    if: github.repository == 'leanprover-community/mathlib4' || github.repository == 'leanprover-community/mathlib4-nightly-testing'
     strategy:
       matrix:
         branch_type: [master, nightly]
@@ -38,7 +42,9 @@ jobs:
       - name: Fetch latest tags (if nightly)
         if: matrix.branch_type == 'nightly'
         run: |
-          git fetch --tags
+          # When in nightly mode, fetch tags from the nightly-testing repository
+          git remote add nightly-testing https://github.com/leanprover-community/mathlib4-nightly-testing.git
+          git fetch nightly-testing --tags
           LATEST_TAG=$(git tag | grep -E "${{ env.TAG_PATTERN }}" | sort -r | head -n 1)
           echo "LATEST_TAG=${LATEST_TAG}" >> "$GITHUB_ENV"
 
@@ -54,6 +60,7 @@ jobs:
       - name: Checkout branch or tag
         uses: actions/checkout@11bd71901bbe5b1630ceea73d27597364c9af683 # v4.2.2
         with:
+          repository: ${{ matrix.branch_type == 'nightly' && 'leanprover-community/mathlib4-nightly-testing' || github.repository }}
           ref: ${{ env.BRANCH_REF }}
 
       - name: Configure Lean
@@ -112,7 +119,7 @@ jobs:
           api-key: ${{ secrets.ZULIP_API_KEY }}
           email: 'github-mathlib4-bot@leanprover.zulipchat.com'
           organization-url: 'https://leanprover.zulipchat.com'
-          to: 'mathlib reviewers'
+          to: 'nightly-testing'
           type: 'stream'
           topic: 'lean4checker'
           content: |
@@ -125,7 +132,7 @@ jobs:
           api-key: ${{ secrets.ZULIP_API_KEY }}
           email: 'github-mathlib4-bot@leanprover.zulipchat.com'
           organization-url: 'https://leanprover.zulipchat.com'
-          to: 'mathlib reviewers'
+          to: 'nightly-testing'
           type: 'stream'
           topic: 'mathlib test executable'
           content: |
@@ -138,7 +145,7 @@ jobs:
           api-key: ${{ secrets.ZULIP_API_KEY }}
           email: 'github-mathlib4-bot@leanprover.zulipchat.com'
           organization-url: 'https://leanprover.zulipchat.com'
-          to: 'mathlib reviewers'
+          to: 'nightly-testing'
           type: 'stream'
           topic: 'lean4checker failure'
           content: |
@@ -152,7 +159,7 @@ jobs:
           api-key: ${{ secrets.ZULIP_API_KEY }}
           email: 'github-mathlib4-bot@leanprover.zulipchat.com'
           organization-url: 'https://leanprover.zulipchat.com'
-          to: 'mathlib reviewers'
+          to: 'nightly-testing'
           type: 'stream'
           topic: 'mathlib test executable failure'
           content: |