Stream: coqbot devs & users

Topic: Lean community bot

view this post on Zulip Karl Palmskog (Jan 07 2022 at 10:28):

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?

view this post on Zulip Théo Zimmermann (Jan 07 2022 at 11:11):

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.

view this post on Zulip Gaëtan Gilbert (Jan 07 2022 at 11:37):

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.

view this post on Zulip Théo Zimmermann (Jan 07 2022 at 12:50):

Hum, so in fact, their "bots" are all Action-based?

Last updated: Apr 20 2024 at 00:02 UTC