nightly#8 adaptations for nightly-2025-06-30

Stream: nightly-testing

[Kim Morrison]

chore: adaptations for nightly-2025-06-30 nightly#8 Please review this PR. At the end of the month this diff will land in 'master'.

[Johan Commelin]

@Damiano Testa Do you think we can easily run a copy of the emoji bot on the testing repo?

[Damiano Testa]

By this you mean automating the that you manually applied above?

[Bryan Gin-ge Chen]

It should be possible if we do the following:

• most of our workflows have a test that they are running in leanprover-community/mathlib4; for the workflows we want to run in the testing repo, we can relax that test
• someone needs to create a new Zulip bot (named e.g. "mathlib4-nightly-testing bot") and add the API key for that bot to the secrets of the testing repo under ZULIP_API_KEY. We could also use the same bot / API key as mathlib4. That one is controlled by @Kim Morrison .

[Damiano Testa]

Could we do this more extensible still, to also include website, blog and whatever other repo we might want in the future? E.g., we could maintain a list of repos where the actions should be performed, so that then the only modification would be extending the list and adding the API key.

[Bryan Gin-ge Chen]

Hmm, I guess we could read a text file or something from somewhere containing a list of repos and then try to match the repo name against that. Though I wonder if it might be worth thinking about re-architecting some of our workflows / scripts so that they could live in a separate repo and then listen to repository_dispatch events from a list of repos that we configure there. This would allow us to move some of the development of workflows outside of mathlib4, as well as potentially making it possible for downstream projects to use some of our automation.

[Damiano Testa]

I like the idea of having a CI repo in leanprover-community!