Just to flag up that apparently the Lean mathlib devs are now using their own bot: https://leanprover-community.github.io/archive/stream/113488-general/topic/leanprover-community-bot-assistant.html
Seems like they are targeting a different set of maintenance tasks, but maybe there is some overlap with coqbot?
Several bots actually: leanprover-community-bot and leanprover-community-bot-assistant. They say that the first one couldn't keep up with all the tasks by itself. I'm curious to know why.
https://github.com/leanprover-community/mathlib/pull/11274
This is an attempt to fix some of the CI failures we're seeing due to GitHub rate limits on the default Actions token.
Hum, so in fact, their "bots" are all Action-based?
Last updated: Sep 28 2023 at 09:01 UTC