Karl Palmskog (Nov 21 2022 at 13:44): 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?
Théo Zimmermann (Nov 21 2022 at 13:45):How do you plan to implement that?
Karl Palmskog (Nov 21 2022 at 13:46):we can just give Gaëtan Write Maintain role in the repos, for example
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. "
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.
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)
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.
Karl Palmskog (Nov 21 2022 at 13:54):OK, that sounds like a good more general solution
Gaëtan Gilbert (Nov 21 2022 at 13:57):what does branch protection change?
Karl Palmskog (Nov 21 2022 at 13:58):regular organization members can't push to master/main anymore
Gaëtan Gilbert (Nov 21 2022 at 13:58):but we use the merge button for overlays, is that affected too?
Karl Palmskog (Nov 21 2022 at 13:58):to my knowledge, yes
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.
Karl Palmskog (Nov 21 2022 at 14:12):we might consider handling MathComp CI projects in Coq-Community analogously
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.
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)
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
Pierre-Marie Pédrot (Nov 21 2022 at 14:27):Organiza-what? Never heard that word.
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
Pierre-Marie Pédrot (Nov 21 2022 at 14:31):true = false, not great, not terrible.
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
Paolo Giarrusso (Nov 21 2022 at 18:00):I think branch protection still allows merging to people that can't push to master?
Paolo Giarrusso (Nov 21 2022 at 18:01):You only need exceptions to branch protection if you want people to bypass MR review.
Karl Palmskog (Nov 21 2022 at 18:16):our standard branch protection rule doesn't have anything to do with "MRs" (PRs)
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.
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.
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.)
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: Jun 03 2023 at 15:31 UTC