Stream: Hierarchy Builder devs & users

Topic: PR bot accounts


view this post on Zulip Karl Palmskog (Sep 20 2023 at 14:34):

it would be good if we didn't have abundance of different bot accounts (that submit PRs)

view this post on Zulip Enrico Tassi (Sep 20 2023 at 14:35):

I reused the coqelpibot one...

view this post on Zulip Enrico Tassi (Sep 20 2023 at 14:35):

but apparently GH considered it a new contributor.

view this post on Zulip Enrico Tassi (Sep 20 2023 at 14:35):

not sure why

view this post on Zulip Karl Palmskog (Sep 20 2023 at 14:36):

OK, that's one less, but there is still vscoqbot, coqelpibot, and some other ones?

view this post on Zulip Notification Bot (Sep 20 2023 at 14:36):

Karl Palmskog has marked this topic as unresolved.

view this post on Zulip Enrico Tassi (Sep 20 2023 at 14:37):

I'm all for using the coq-community one, but I don't know if this is already a thing, and also HB is not in CC

view this post on Zulip Karl Palmskog (Sep 20 2023 at 14:37):

ah, so we will need one per org? I was hoping we could reuse coqbot all over the place, but I think Théo already mentioned some restrictions

view this post on Zulip Enrico Tassi (Sep 20 2023 at 14:38):

I guess we can use just one, but maybe sharing secretes is easier if the org is the same

view this post on Zulip Karl Palmskog (Sep 20 2023 at 14:41):

could we maybe use some future Coq Call to try to coordinate this kind of automation a bit? E.g., at least me, Théo, Romain, Enrico

view this post on Zulip Karl Palmskog (Sep 20 2023 at 14:42):

others will probably be bored out of their minds, so best to flag up well ahead

view this post on Zulip Enrico Tassi (Sep 20 2023 at 14:43):

Enrico Tassi said:

but apparently GH considered it a new contributor.

because the other PR was not merged (but closed, since it was a test).

view this post on Zulip Karl Palmskog (Sep 20 2023 at 14:43):

apparently CI was triggered, so new vs. old contributors don't matter in Coq opam archive, but maybe it should

view this post on Zulip Enrico Tassi (Sep 20 2023 at 16:56):

I did unblock it by hand


Last updated: Apr 21 2024 at 01:02 UTC