Skip to content

Commit dbe9b5a

Browse files
kim-emkim-em
committed
chore: route Zulip notifications to nightly-testing-mathlib (leanprover-community#38946)
This PR retargets every Zulip-posting CI workflow in mathlib4 from the shared `nightly-testing` channel to the new project-specific `#nightly-testing-mathlib` channel, in line with the [proposal to split `#nightly-testing`](https://leanprover.zulipchat.com/#narrow/channel/428973-nightly-testing/topic/proposal.20to.20split.20the.20channel/near/592721807) 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). The `#nightly-testing-mathlib` channel mirrors the original (web-public, history visible to subscribers, anyone can post). Companion PRs for `mathlib-ci`, `batteries`, and `cslib` are coming next. 🤖 Prepared with Claude Code
1 parent d2df507 commit dbe9b5a

7 files changed

Lines changed: 21 additions & 21 deletions

‎.github/workflows/daily.yml‎

Lines changed: 6 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -127,7 +127,7 @@ jobs:
127127
api-key: ${{ secrets.ZULIP_API_KEY }}
128128
email: 'github-mathlib4-bot@leanprover.zulipchat.com'
129129
organization-url: 'https://leanprover.zulipchat.com'
130-
to: 'nightly-testing'
130+
to: 'nightly-testing-mathlib'
131131
type: 'stream'
132132
topic: 'leanchecker'
133133
content: |
@@ -140,7 +140,7 @@ jobs:
140140
api-key: ${{ secrets.ZULIP_API_KEY }}
141141
email: 'github-mathlib4-bot@leanprover.zulipchat.com'
142142
organization-url: 'https://leanprover.zulipchat.com'
143-
to: 'nightly-testing'
143+
to: 'nightly-testing-mathlib'
144144
type: 'stream'
145145
topic: 'leanchecker failure'
146146
content: |
@@ -250,7 +250,7 @@ jobs:
250250
api-key: ${{ secrets.ZULIP_API_KEY }}
251251
email: 'github-mathlib4-bot@leanprover.zulipchat.com'
252252
organization-url: 'https://leanprover.zulipchat.com'
253-
to: 'nightly-testing'
253+
to: 'nightly-testing-mathlib'
254254
type: 'stream'
255255
topic: 'mathlib test executable'
256256
content: |
@@ -263,7 +263,7 @@ jobs:
263263
api-key: ${{ secrets.ZULIP_API_KEY }}
264264
email: 'github-mathlib4-bot@leanprover.zulipchat.com'
265265
organization-url: 'https://leanprover.zulipchat.com'
266-
to: 'nightly-testing'
266+
to: 'nightly-testing-mathlib'
267267
type: 'stream'
268268
topic: 'mathlib test executable failure'
269269
content: |
@@ -415,7 +415,7 @@ jobs:
415415
api-key: ${{ secrets.ZULIP_API_KEY }}
416416
email: 'github-mathlib4-bot@leanprover.zulipchat.com'
417417
organization-url: 'https://leanprover.zulipchat.com'
418-
to: 'nightly-testing'
418+
to: 'nightly-testing-mathlib'
419419
type: 'stream'
420420
topic: 'nanoda'
421421
content: |
@@ -428,7 +428,7 @@ jobs:
428428
api-key: ${{ secrets.ZULIP_API_KEY }}
429429
email: 'github-mathlib4-bot@leanprover.zulipchat.com'
430430
organization-url: 'https://leanprover.zulipchat.com'
431-
to: 'nightly-testing'
431+
to: 'nightly-testing-mathlib'
432432
type: 'stream'
433433
topic: 'nanoda failure'
434434
content: |

‎.github/workflows/nightly_bump_and_merge.yml‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -360,7 +360,7 @@ jobs:
360360
api-key: ${{ secrets.ZULIP_API_KEY }}
361361
email: 'github-mathlib4-bot@leanprover.zulipchat.com'
362362
organization-url: 'https://leanprover.zulipchat.com'
363-
to: 'nightly-testing'
363+
to: 'nightly-testing-mathlib'
364364
type: 'stream'
365365
topic: 'Mergeable lean testing PRs'
366366
content: |

‎.github/workflows/nightly_detect_failure.yml‎

Lines changed: 6 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -21,7 +21,7 @@ jobs:
2121
api-key: ${{ secrets.ZULIP_API_KEY }}
2222
email: 'github-mathlib4-bot@leanprover.zulipchat.com'
2323
organization-url: 'https://leanprover.zulipchat.com'
24-
to: 'nightly-testing'
24+
to: 'nightly-testing-mathlib'
2525
type: 'stream'
2626
topic: 'Mathlib status updates'
2727
content: |
@@ -159,7 +159,7 @@ jobs:
159159
'num_before': 1,
160160
'num_after': 0,
161161
'narrow': [
162-
{'operator': 'stream', 'operand': 'nightly-testing'},
162+
{'operator': 'stream', 'operand': 'nightly-testing-mathlib'},
163163
{'operator': 'topic', 'operand': 'Mathlib status updates'},
164164
{'operator': 'sender', 'operand': bot_email}
165165
],
@@ -171,7 +171,7 @@ jobs:
171171
# Post the success message
172172
request = {
173173
'type': 'stream',
174-
'to': 'nightly-testing',
174+
'to': 'nightly-testing-mathlib',
175175
'topic': 'Mathlib status updates',
176176
'content': f"✅ The latest CI for Mathlib's [nightly-testing branch](https://github.com/leanprover-community/mathlib4-nightly-testing/tree/nightly-testing) has succeeded! ([{os.getenv('SHA')}](https://github.com/${{ github.repository }}/commit/{os.getenv('SHA')}))"
177177
}
@@ -310,7 +310,7 @@ jobs:
310310
api-key: ${{ secrets.ZULIP_API_KEY }}
311311
email: 'github-mathlib4-bot@leanprover.zulipchat.com'
312312
organization-url: 'https://leanprover.zulipchat.com'
313-
to: 'nightly-testing'
313+
to: 'nightly-testing-mathlib'
314314
type: 'stream'
315315
topic: 'Mathlib status updates'
316316
content: |
@@ -435,7 +435,7 @@ jobs:
435435
'num_before': 1,
436436
'num_after': 0,
437437
'narrow': [
438-
{'operator': 'stream', 'operand': 'nightly-testing'},
438+
{'operator': 'stream', 'operand': 'nightly-testing-mathlib'},
439439
{'operator': 'topic', 'operand': 'Mathlib bump branch reminders'},
440440
{'operator': 'sender', 'operand': bot_email}
441441
],
@@ -473,7 +473,7 @@ jobs:
473473
# Post the reminder message
474474
request = {
475475
'type': 'stream',
476-
'to': 'nightly-testing',
476+
'to': 'nightly-testing-mathlib',
477477
'topic': 'Mathlib bump branch reminders',
478478
'content': payload
479479
}

‎.github/workflows/remove_deprecated_decls.yml‎

Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -200,7 +200,7 @@ jobs:
200200
api-key: ${{ secrets.ZULIP_API_KEY }}
201201
email: 'github-mathlib4-bot@leanprover.zulipchat.com'
202202
organization-url: 'https://leanprover.zulipchat.com'
203-
to: 'nightly-testing'
203+
to: 'nightly-testing-mathlib'
204204
type: 'stream'
205205
topic: 'Mathlib `remove outdated deprecated declarations`'
206206
content: |
@@ -247,7 +247,7 @@ jobs:
247247
api-key: ${{ secrets.ZULIP_API_KEY }}
248248
email: 'github-mathlib4-bot@leanprover.zulipchat.com'
249249
organization-url: 'https://leanprover.zulipchat.com'
250-
to: 'nightly-testing'
250+
to: 'nightly-testing-mathlib'
251251
type: 'stream'
252252
topic: 'Mathlib `remove outdated deprecated declarations`'
253253
content: |
@@ -261,7 +261,7 @@ jobs:
261261
api-key: ${{ secrets.ZULIP_API_KEY }}
262262
email: 'github-mathlib4-bot@leanprover.zulipchat.com'
263263
organization-url: 'https://leanprover.zulipchat.com'
264-
to: 'nightly-testing'
264+
to: 'nightly-testing-mathlib'
265265
type: 'stream'
266266
topic: 'Mathlib `remove outdated deprecated declarations`'
267267
content: |

‎.github/workflows/rm_set_option.yml‎

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -136,7 +136,7 @@ jobs:
136136
api-key: ${{ secrets.ZULIP_API_KEY }}
137137
email: 'github-mathlib4-bot@leanprover.zulipchat.com'
138138
organization-url: 'https://leanprover.zulipchat.com'
139-
to: 'nightly-testing'
139+
to: 'nightly-testing-mathlib'
140140
type: 'stream'
141141
topic: 'Mathlib `remove unnecessary set_option lines`'
142142
content: |
@@ -149,7 +149,7 @@ jobs:
149149
api-key: ${{ secrets.ZULIP_API_KEY }}
150150
email: 'github-mathlib4-bot@leanprover.zulipchat.com'
151151
organization-url: 'https://leanprover.zulipchat.com'
152-
to: 'nightly-testing'
152+
to: 'nightly-testing-mathlib'
153153
type: 'stream'
154154
topic: 'Mathlib `remove unnecessary set_option lines`'
155155
content: |

‎.github/workflows/update_dependencies.yml‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -211,7 +211,7 @@ jobs:
211211
api-key: ${{ secrets.ZULIP_API_KEY }}
212212
email: 'github-mathlib4-bot@leanprover.zulipchat.com'
213213
organization-url: 'https://leanprover.zulipchat.com'
214-
to: 'nightly-testing'
214+
to: 'nightly-testing-mathlib'
215215
type: 'stream'
216216
topic: 'Mathlib `lake update` failure'
217217
content: |

‎.github/workflows/update_dependencies_zulip.yml‎

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -94,7 +94,7 @@ jobs:
9494
api-key: ${{ secrets.ZULIP_API_KEY }}
9595
email: 'github-mathlib4-bot@leanprover.zulipchat.com'
9696
organization-url: 'https://leanprover.zulipchat.com'
97-
to: 'nightly-testing'
97+
to: 'nightly-testing-mathlib'
9898
type: 'stream'
9999
topic: 'Mathlib `lake update` failure'
100100
content: |
@@ -173,7 +173,7 @@ jobs:
173173
api-key: ${{ secrets.ZULIP_API_KEY }}
174174
email: 'github-mathlib4-bot@leanprover.zulipchat.com'
175175
organization-url: 'https://leanprover.zulipchat.com'
176-
to: 'nightly-testing'
176+
to: 'nightly-testing-mathlib'
177177
type: 'stream'
178178
topic: 'Mathlib `lake update` success'
179179
content: |

0 commit comments

Comments
 (0)