Stream: coq-community devs & users

Topic: Backup merging for Coq CI projects


view this post on Zulip Karl Palmskog (Nov 21 2022 at 13:44):

@Gaëtan Gilbert @Théo Zimmermann we now have quite a few projects that are in Coq's CI in Coq-community. At the same time, we are adding branch protection to a lot of projects. I propose that we add Gaëtan as "backup merger" to the Coq CI projects that have branch protection. This way, Coq core devs don't have to wait for Théo or me to handle urgent merges. Can/should we add someone else from core team as well?

view this post on Zulip Théo Zimmermann (Nov 21 2022 at 13:45):

How do you plan to implement that?

view this post on Zulip Karl Palmskog (Nov 21 2022 at 13:46):

we can just give Gaëtan Write Maintain role in the repos, for example

view this post on Zulip Karl Palmskog (Nov 21 2022 at 13:47):

how I handle branch protection in my projects is to restrict master pushes to "Organization administrators, repository administrators, and users with the Maintain role. "

view this post on Zulip Karl Palmskog (Nov 21 2022 at 13:49):

I think we should also consistently use the coq-ci GitHub topic for projects in the CI.

view this post on Zulip Karl Palmskog (Nov 21 2022 at 13:50):

@Gaëtan Gilbert are you fine with this then? If so, you'll just get some GitHub notifications as I add this role (Maintain)

view this post on Zulip Théo Zimmermann (Nov 21 2022 at 13:53):

I just created a team called "Coq overlays mergers". You could give it maintain access to the repositories with the coq-ci topic. This would avoid doing it manually for each allowed Coq dev merger.

view this post on Zulip Karl Palmskog (Nov 21 2022 at 13:54):

OK, that sounds like a good more general solution

view this post on Zulip Gaëtan Gilbert (Nov 21 2022 at 13:57):

what does branch protection change?

view this post on Zulip Karl Palmskog (Nov 21 2022 at 13:58):

regular organization members can't push to master/main anymore

view this post on Zulip Gaëtan Gilbert (Nov 21 2022 at 13:58):

but we use the merge button for overlays, is that affected too?

view this post on Zulip Karl Palmskog (Nov 21 2022 at 13:58):

to my knowledge, yes

view this post on Zulip Karl Palmskog (Nov 21 2022 at 14:11):

@Théo Zimmermann I went through and added all missing coq-ci topics and also added the team with Maintain role, even if there was no branch protection. Maybe you can discuss in Core who should be in the merger team.

view this post on Zulip Karl Palmskog (Nov 21 2022 at 14:12):

we might consider handling MathComp CI projects in Coq-Community analogously

view this post on Zulip Théo Zimmermann (Nov 21 2022 at 14:12):

Oh, that probably does not need to be a private discussion. I guess we could add Pierre-Marie besides Gaëtan.

view this post on Zulip Karl Palmskog (Nov 21 2022 at 14:13):

sure, I'm just saying, please solve however you like and no need to keep me involved (other than if I should edit something in a repo)

view this post on Zulip Karl Palmskog (Nov 21 2022 at 14:18):

I'm always mentally picturing a "Core control room" where work is organized in detail and handed out centrally, but I'm sure it's more simple than that

view this post on Zulip Pierre-Marie Pédrot (Nov 21 2022 at 14:27):

Organiza-what? Never heard that word.

view this post on Zulip Karl Palmskog (Nov 21 2022 at 14:29):

and as soon as there is a soundness bug, there is a siren that starts to blare and emit red light

view this post on Zulip Pierre-Marie Pédrot (Nov 21 2022 at 14:31):

true = false, not great, not terrible.

view this post on Zulip Karl Palmskog (Nov 21 2022 at 14:35):

I remember Twitter used to have a "Fail whale", maybe someone can do a similar picture for Coq that is posted in each consistency issue

view this post on Zulip Paolo Giarrusso (Nov 21 2022 at 18:00):

I think branch protection still allows merging to people that can't push to master?

view this post on Zulip Paolo Giarrusso (Nov 21 2022 at 18:01):

You only need exceptions to branch protection if you want people to bypass MR review.

view this post on Zulip Karl Palmskog (Nov 21 2022 at 18:16):

our standard branch protection rule doesn't have anything to do with "MRs" (PRs)

view this post on Zulip Karl Palmskog (Nov 21 2022 at 18:37):

but more generally, I think we want to allow repo admins to select precisely the branch protection rule they want, while still letting the core team merge overlays if the project is in Coq's CI.

view this post on Zulip John Wiegley (Nov 23 2022 at 17:29):

Karl Palmskog said:

I propose that we add Gaëtan as "backup merger" to the Coq CI projects that have branch protection.

Does this include community projects like mine? Since being added to Coq CI I now require all changes to master to go through a PR, including for my own development, just to ensure that I'm never the cause of Coq's CI breaking.

view this post on Zulip Karl Palmskog (Nov 23 2022 at 17:51):

@John Wiegley we are only talking about the Coq-community organization on GitHub: https://github.com/coq-community/

As far as I know, GitHub Teams (which we are using here) can only be defined inside GitHub organizations. The projects inside the organization can have a wide variety of branch protection rules, so defining a team specifically for the subset of projects that happen to be in Coq's CI makes sense for us.

(Incidentally, our GitHub organization is open to transfers of new Coq projects of general interest for increased collaborative maintenance, https://github.com/coq-community/manifesto#collaborative-maintenance-of-coq-packages-and-tools - let us know if you are interested in this.)

view this post on Zulip Karl Palmskog (Nov 23 2022 at 17:55):

for example, in the Coq-community projects I maintain, I set the branch protection for master so only me and my co-maintainers can push to master, regardless of PRs.


Last updated: Feb 05 2023 at 13:02 UTC