From 133b883b37316dbc2c288e4a34b489cd3a5cd2f5 Mon Sep 17 00:00:00 2001
From: Kim Morrison <kim@tqft.net>
Date: Tue, 5 May 2026 12:48:39 +1000
Subject: [PATCH 1/2] chore: route Zulip notifications to nightly-testing-cslib
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

This PR retargets the nightly-testing failure-detection workflow and the
adaptation-PR helper script from the shared `nightly-testing` channel to the
new `nightly-testing-cslib` channel, in line with the proposal to split
`#nightly-testing` into per-project channels for Mathlib, Batteries, and Cslib.

Topic names are unchanged so existing bookmarks and topic links continue to
resolve to the same conversations (which were also moved over).

🤖 Prepared with Claude Code
---
 .../workflows/report_failures_nightly-testing.yml    | 12 ++++++------
 scripts/create-adaptation-pr.sh                      |  2 +-
 2 files changed, 7 insertions(+), 7 deletions(-)

diff --git a/.github/workflows/report_failures_nightly-testing.yml b/.github/workflows/report_failures_nightly-testing.yml
index bdbd87881..edeeb9168 100644
--- a/.github/workflows/report_failures_nightly-testing.yml
+++ b/.github/workflows/report_failures_nightly-testing.yml
@@ -21,7 +21,7 @@ jobs:
         api-key: ${{ secrets.ZULIP_API_KEY }}
         email: 'github-mathlib4-bot@leanprover.zulipchat.com'
         organization-url: 'https://leanprover.zulipchat.com'
-        to: 'nightly-testing'
+        to: 'nightly-testing-cslib'
         type: 'stream'
         topic: 'Cslib status updates'
         content: |
@@ -101,7 +101,7 @@ jobs:
           'num_before': 1,
           'num_after': 0,
           'narrow': [
-            {'operator': 'stream', 'operand': 'nightly-testing'},
+            {'operator': 'stream', 'operand': 'nightly-testing-cslib'},
             {'operator': 'topic', 'operand': 'Cslib status updates'},
             {'operator': 'sender', 'operand': bot_email}
           ],
@@ -113,7 +113,7 @@ jobs:
             # Post the success message
             request = {
                 'type': 'stream',
-                'to': 'nightly-testing',
+                'to': 'nightly-testing-cslib',
                 'topic': 'Cslib status updates',
                 'content': f"✅ The latest CI for Cslib's [nightly-testing branch](https://github.com/leanprover/cslib/tree/nightly-testing) has succeeded! ([{os.getenv('SHA')}](https://github.com/${{ github.repository }}/commit/{os.getenv('SHA')}))"
             }
@@ -250,7 +250,7 @@ jobs:
         api-key: ${{ secrets.ZULIP_API_KEY }}
         email: 'github-mathlib4-bot@leanprover.zulipchat.com'
         organization-url: 'https://leanprover.zulipchat.com'
-        to: 'nightly-testing'
+        to: 'nightly-testing-cslib'
         type: 'stream'
         topic: 'Cslib status updates'
         content: |
@@ -350,7 +350,7 @@ jobs:
               'num_before': 1,
               'num_after': 0,
               'narrow': [
-                {'operator': 'stream', 'operand': 'nightly-testing'},
+                {'operator': 'stream', 'operand': 'nightly-testing-cslib'},
                 {'operator': 'topic', 'operand': 'Cslib bump branch reminders'},
                 {'operator': 'sender', 'operand': bot_email}
               ],
@@ -388,7 +388,7 @@ jobs:
                 # Post the reminder message
                 request = {
                     'type': 'stream',
-                    'to': 'nightly-testing',
+                    'to': 'nightly-testing-cslib',
                     'topic': 'Cslib bump branch reminders',
                     'content': payload
                 }
diff --git a/scripts/create-adaptation-pr.sh b/scripts/create-adaptation-pr.sh
index 01587009c..4c867feb9 100755
--- a/scripts/create-adaptation-pr.sh
+++ b/scripts/create-adaptation-pr.sh
@@ -209,7 +209,7 @@ if git diff --name-only bump/"$BUMPVERSION" bump/nightly-"$NIGHTLYDATE" | grep -
   echo " Body: $zulip_body"
 
   if command -v zulip-send >/dev/null 2>&1; then
-    zulip_command="zulip-send --stream nightly-testing --subject \"$zulip_title\" --message \"$zulip_body\""
+    zulip_command="zulip-send --stream nightly-testing-cslib --subject \"$zulip_title\" --message \"$zulip_body\""
     echo "Running the following 'zulip-send' command to do this:"
     echo "> $zulip_command"
     eval "$zulip_command"

From 31ad6e106c993e9c28c49864ee7da629bbd93e4d Mon Sep 17 00:00:00 2001
From: Kim Morrison <kim@tqft.net>
Date: Tue, 5 May 2026 13:11:39 +1000
Subject: [PATCH 2/2] chore: update echo string to reference new channel name
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

Codex review caught that the prose `echo` still referenced the old
`#nightly-testing` channel even though the actual `zulip-send` call was
already retargeted at `#nightly-testing-cslib`.

🤖 Prepared with Claude Code
---
 scripts/create-adaptation-pr.sh | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/scripts/create-adaptation-pr.sh b/scripts/create-adaptation-pr.sh
index 4c867feb9..47b1ee2a1 100755
--- a/scripts/create-adaptation-pr.sh
+++ b/scripts/create-adaptation-pr.sh
@@ -203,7 +203,7 @@ if git diff --name-only bump/"$BUMPVERSION" bump/nightly-"$NIGHTLYDATE" | grep -
   zulip_title="cslib#$pr_number adaptations for nightly-$NIGHTLYDATE"
   zulip_body=$(printf "> %s\n\nPlease review this PR. At the end of the month this diff will land in 'main'." "$pr_title cslib#$pr_number")
 
-  echo "Posting the link to the PR in a new thread on the #nightly-testing channel on Zulip"
+  echo "Posting the link to the PR in a new thread on the #nightly-testing-cslib channel on Zulip"
   echo "Here is the message:"
   echo "Title: $zulip_title"
   echo " Body: $zulip_body"