@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?
How do you plan to implement that?
we can just give Gaëtan
Write Maintain role in the repos, for example
how I handle branch protection in my projects is to restrict
master pushes to "Organization administrators, repository administrators, and users with the Maintain role. "
I think we should also consistently use the
coq-ci GitHub topic for projects in the CI.
@Gaëtan Gilbert are you fine with this then? If so, you'll just get some GitHub notifications as I add this role (Maintain)
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.
OK, that sounds like a good more general solution
what does branch protection change?
regular organization members can't push to
but we use the merge button for overlays, is that affected too?
to my knowledge, yes
@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.
we might consider handling MathComp CI projects in Coq-Community analogously
Oh, that probably does not need to be a private discussion. I guess we could add Pierre-Marie besides Gaëtan.
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)
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
Organiza-what? Never heard that word.
and as soon as there is a soundness bug, there is a siren that starts to blare and emit red light
true = false, not great, not terrible.
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
I think branch protection still allows merging to people that can't push to master?
You only need exceptions to branch protection if you want people to bypass MR review.
our standard branch protection rule doesn't have anything to do with "MRs" (PRs)
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.
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.
@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.)
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