From 8fe068ef6834373f4b4739f325121c1e487fafe2 Mon Sep 17 00:00:00 2001
From: Kim Morrison <477956+kim-em@users.noreply.github.com>
Date: Tue, 24 Jun 2025 13:30:43 +1000
Subject: [PATCH] feat: move lean-pr-testing-NNNN branches to a fork (#8933)

This PR changes the CI setup to generate `lean-pr-testing-NNNN` branches
for Mathlib on the `leanprover-community/mathlib4-nightly-testing` fork,
rather than on the main repo.
---
 .github/workflows/ci.yml         | 2 +-
 .github/workflows/pr-release.yml | 4 ++--
 doc/dev/index.md                 | 3 ++-
 script/mathlib-bench             | 9 ++++++---
 tests/lean/run/grind_trig.lean   | 2 +-
 5 files changed, 12 insertions(+), 8 deletions(-)

diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml
index f0a3e187f4..615ef1883f 100644
--- a/.github/workflows/ci.yml
+++ b/.github/workflows/ci.yml
@@ -421,6 +421,6 @@ jobs:
           GITHUB_TOKEN: ${{ secrets.RELEASE_INDEX_TOKEN }}
       - name: Update toolchain on mathlib4's nightly-testing branch
         run: |
-          gh workflow -R leanprover-community/mathlib4 run nightly_bump_toolchain.yml
+          gh workflow -R leanprover-community/mathlib4-nightly-testing run nightly_bump_toolchain.yml
         env:
           GITHUB_TOKEN: ${{ secrets.MATHLIB4_BOT }}
diff --git a/.github/workflows/pr-release.yml b/.github/workflows/pr-release.yml
index 3b821f1409..07ab4973ba 100644
--- a/.github/workflows/pr-release.yml
+++ b/.github/workflows/pr-release.yml
@@ -167,7 +167,7 @@ jobs:
             echo "The merge base of this PR coincides with the nightly release"
 
             BATTERIES_REMOTE_TAGS="$(git ls-remote https://github.com/leanprover-community/batteries.git nightly-testing-"$MOST_RECENT_NIGHTLY")"
-            MATHLIB_REMOTE_TAGS="$(git ls-remote https://github.com/leanprover-community/mathlib4.git nightly-testing-"$MOST_RECENT_NIGHTLY")"
+            MATHLIB_REMOTE_TAGS="$(git ls-remote https://github.com/leanprover-community/mathlib4-nightly-testing.git nightly-testing-"$MOST_RECENT_NIGHTLY")"
 
             if [[ -n "$BATTERIES_REMOTE_TAGS" ]]; then
               echo "... and Batteries has a 'nightly-testing-$MOST_RECENT_NIGHTLY' tag."
@@ -355,7 +355,7 @@ jobs:
         if: steps.workflow-info.outputs.pullRequestNumber != '' && steps.ready.outputs.mathlib_ready == 'true'
         uses: actions/checkout@v4
         with:
-          repository: leanprover-community/mathlib4
+          repository: leanprover-community/mathlib4-nightly-testing
           token: ${{ secrets.MATHLIB4_BOT }}
           ref: nightly-testing
           fetch-depth: 0 # This ensures we check out all tags and branches.
diff --git a/doc/dev/index.md b/doc/dev/index.md
index ea626f23a4..f97d993b27 100644
--- a/doc/dev/index.md
+++ b/doc/dev/index.md
@@ -85,5 +85,6 @@ such that changing files in `Init` doesn't force a full rebuild of `Lean`.
 You can test a Lean PR against Mathlib and Batteries by rebasing your PR
 on to `nightly-with-mathlib` branch. (It is fine to force push after rebasing.)
 CI will generate a branch of Mathlib and Batteries called `lean-pr-testing-NNNN`
-that uses the toolchain for your PR, and will report back to the Lean PR with results from Mathlib CI.
+on the `leanprover-community/mathlib4-nightly-testing` fork of Mathlib.
+This branch uses the toolchain for your PR, and will report back to the Lean PR with results from Mathlib CI.
 See https://leanprover-community.github.io/contribute/tags_and_branches.html for more details.
diff --git a/script/mathlib-bench b/script/mathlib-bench
index b065a9aa56..b8cb1e15b6 100755
--- a/script/mathlib-bench
+++ b/script/mathlib-bench
@@ -5,8 +5,11 @@ set -euo pipefail
 
 [ $# -eq 1 ] || (echo "usage: $0 <lean4 PR #>"; exit 1)
 
+echo "Warning: the speedcenter is probably not listening on mathlib4-nightly-testing yet."
+echo "If you're using this script, please contact @kim-em or @Kha to get this set up, and then remove this notice."
+
 LEAN_PR=$1
-PR_RESPONSE=$(gh api repos/leanprover-community/mathlib4/pulls -X POST -f head=lean-pr-testing-$LEAN_PR -f base=nightly-testing -f title="leanprover/lean4#$LEAN_PR benchmarking" -f draft=true -f body="ignore me")
+PR_RESPONSE=$(gh api repos/leanprover-community/mathlib4-nightly-testing/pulls -X POST -f head=lean-pr-testing-$LEAN_PR -f base=nightly-testing -f title="leanprover/lean4#$LEAN_PR benchmarking" -f draft=true -f body="ignore me")
 PR_NUMBER=$(echo "$PR_RESPONSE" | jq '.number')
-echo "opened https://github.com/leanprover-community/mathlib4/pull/$PR_NUMBER"
-gh api repos/leanprover-community/mathlib4/issues/$PR_NUMBER/comments -X POST -f body="!bench" > /dev/null
+echo "opened https://github.com/leanprover-community/mathlib4-nightly-testing/pull/$PR_NUMBER"
+gh api repos/leanprover-community/mathlib4-nightly-testing/issues/$PR_NUMBER/comments -X POST -f body="!bench" > /dev/null
diff --git a/tests/lean/run/grind_trig.lean b/tests/lean/run/grind_trig.lean
index a53a3c0752..2dd3035a50 100644
--- a/tests/lean/run/grind_trig.lean
+++ b/tests/lean/run/grind_trig.lean
@@ -30,5 +30,5 @@ example (f : R → Nat) : 4 * f ((cos x + sin x)^2) ≠ 2 + f (2 * cos x * sin x
 example (f : R → Nat) : max 3 (4 * f ((cos x + sin x)^2)) ≠ 2 + f (2 * cos x * sin x + 1) := by
   grind
 
--- See https://github.com/leanprover-community/mathlib4/blob/nightly-testing/MathlibTest/grind/trig.lean
+-- See https://github.com/leanprover-community/mathlib4-nightly-testing/blob/nightly-testing/MathlibTest/grind/trig.lean
 -- for the Mathlib version of this test, using the real `ℝ`, `cos`, `sin`, and `cos_sq_and_sin_sq` declarations.