Théo Zimmermann (Apr 19 2023 at 19:33): Théo Zimmermann (Apr 19 2023 at 19:33):GitHub has introduced a new feature called "rulesets" that can be used instead of "protected branches" to achieve similar objectives: https://docs.github.com/en/repositories/configuring-branches-and-merges-in-your-repository/managing-rulesets/about-rulesets
I have replaced our existing protected branch rules with new rulesets.
One advantage is that now everyone can see and understand the rules that apply to branches: https://github.com/coq/coq/rules
Another advantage is that now the rule that prevent creating new branches will apply to everyone, including admins (no more accidental pushing @Matthieu Sozeau!).
Finally, there is now a ruleset restricting who can create and update tags.
I wouldn't mind a review of the rulesets that I have created to check whether they match common expectations.
Gaëtan Gilbert (Apr 19 2023 at 19:43):cool
Jason Gross (Apr 19 2023 at 23:27):Shouldn't coqbot be granted bypass rights on pushing to master without a PR? Or does "Require all commits be made to a non-target branch and submitted via a pull request before they can be merged." mean that commits can be pushed to master by anyone with push rights, so long as a PR exists in which the commit is part of the history?
Jason Gross (Apr 19 2023 at 23:29):Is GitHub displaying negation by showing an x? How does it deal with associativity in patterns? (It took me a moment to figure out that https://github.com/coq/coq/rules/3017 matches "everything except v." rather than "everything matching v.")
Jason Gross (Apr 19 2023 at 23:31):Does https://github.com/coq/coq/rules/3026 "Only allow users with bypass permission to update matching refs." seems to imply that coqbot needs to be an admin to merge PRs into v.? (And don't we need to allow RMs/devs to merge PRs into old branches (without going through coqbot?), even without being admins?)
Jason Gross (Apr 19 2023 at 23:32):Should https://github.com/coq/coq/rules/3041 apply to release branches and not just master?
Jason Gross (Apr 19 2023 at 23:32):Should there be rulesets about tag creation?
Théo Zimmermann (Apr 20 2023 at 07:22):Jason Gross said:
Shouldn't coqbot be granted bypass rights on pushing to master without a PR? Or does "Require all commits be made to a non-target branch and submitted via a pull request before they can be merged." mean that commits can be pushed to master by anyone with push rights, so long as a PR exists in which the commit is part of the history?
Indeed, that's what it means AFAICT. But if we end up implementing the idea discussed in https://coq.zulipchat.com/#narrow/stream/243318-coqbot-devs-.26-users/topic/Automatically.20cleanup.20overlays.3F, then yes you are right that coqbot should be granted bypass rights to push directly for this to work.
Théo Zimmermann (Apr 20 2023 at 08:29):Jason Gross said:
Is GitHub displaying negation by showing an x? How does it deal with associativity in patterns? (It took me a moment to figure out that https://github.com/coq/coq/rules/3017 matches "everything except v." rather than "everything matching v.")
Yes. Not sure what you mean by associativity in patterns.
Théo Zimmermann (Apr 20 2023 at 08:33):Jason Gross said:
Does https://github.com/coq/coq/rules/3026 "Only allow users with bypass permission to update matching refs." seems to imply that coqbot needs to be an admin to merge PRs into v.? (And don't we need to allow RMs/devs to merge PRs into old branches (without going through coqbot?), even without being admins?)
coqbot does not support merging to branches other than master anyway. And we maintain an equivalence between organization owners and core devs, so I think this match our current processes for managing old branches. Regarding branches that are actively maintained by a release manager, until now we have always picked release managers in the core team, so I think this is fine (unless we start doing things differently).
Théo Zimmermann (Apr 20 2023 at 08:34):Jason Gross said:
Should https://github.com/coq/coq/rules/3041 apply to release branches and not just master?
No, because @coq/pushers can only merge pull requests in master. To merge in release branch, you should be the RM (for actively maintained branches) or a core dev (for older branches).
Théo Zimmermann (Apr 20 2023 at 08:34):There is one: https://github.com/coq/coq/rules/3016
Théo Zimmermann (Apr 20 2023 at 08:34):Thanks a lot for all the feedback!
Jason Gross (Apr 20 2023 at 19:34):Théo Zimmermann said:
There is one: https://github.com/coq/coq/rules/3016
Should we also restrict tag creation (without allowing bypass) to V*.* tags? (This will prevent accidental creation of tags without the V, with a lowercase v, etc)
Théo Zimmermann (Apr 21 2023 at 07:18):Indeed, good idea. I'll add a rule for this.
Théo Zimmermann (Apr 21 2023 at 07:40):Done. I've also updated some other rulesets to be more explicit about who can bypass the rule (coq/core) instead of using the "organization and repository admin" bypass: https://github.com/coq/coq/rules
Théo Zimmermann (Apr 24 2023 at 17:15):Apparently, the rulesets are preventing coqbot's merge now feature, but I don't get why.
Théo Zimmermann (Apr 24 2023 at 17:20):I don't understand why when I tried to merge the PR which coqbot couldn't merge with the merge script and pushed, I got:
remote: Resolving deltas: 100% (30/30), completed with 27 local objects.
remote: Bypassed rule violations for refs/heads/master:
remote:
remote: - Cannot update this protected ref
remote:
To github.com:coq/coq
9368fc2424..3e70115359 master -> master
But for coqbot-app, it didn't work.
Théo Zimmermann (Apr 24 2023 at 17:23):This might be a bug with the rulesets, as I don't see any other explanation. We might need to go back to classic branch protection for master so that the feature works again.
Théo Zimmermann (Apr 24 2023 at 17:25):I need to get off the keyboard, but anyone feel free to report this to GitHub and / or remove the ruleset in favor of a branch protection for master. If nobody does it, I'll probably take care of this tomorrow.
Jason Gross (Apr 24 2023 at 22:41):Is going back to classic branch protection better than adding coqbot to the list of users who can bypass https://github.com/coq/coq/rules/3040 ("Require pull requests to commit to master (for everyone)")?
Théo Zimmermann (Apr 25 2023 at 09:26):coqbot-app is already in there. AFAICT, coqbot (the user account) is not the one that merges PRs, it is coqbot-app (the GitHub App), so adding coqbot there wouldn't change anything.
Gaëtan Gilbert (Apr 25 2023 at 11:23):why does https://github.com/coq/coq/settings/rules/3041 have "restrict deletions" and "block force pushes", they're already in https://github.com/coq/coq/settings/rules/3030
Gaëtan Gilbert (Apr 25 2023 at 11:26):anyway I'm disabling https://github.com/coq/coq/settings/rules/3041 and adding a branch protection to master
Gaëtan Gilbert (Apr 25 2023 at 11:28):that didn't work, reverting
Gaëtan Gilbert (Apr 25 2023 at 11:30):oh I didn't actually hit save on the disable, let's try again x_x
Gaëtan Gilbert (Apr 25 2023 at 11:31):ok that worked
Théo Zimmermann (Apr 25 2023 at 11:42):Gaëtan Gilbert said:
why does https://github.com/coq/coq/settings/rules/3041 have "restrict deletions" and "block force pushes", they're already in https://github.com/coq/coq/settings/rules/3030
GitHub puts them by default, and I thought there is no harm in having this kind of restrictions redundantly defined in case we need to temporarily disable one ruleset.
Théo Zimmermann (Apr 25 2023 at 11:43):Thanks for testing this. I will report the bug to GitHub's staff.
Gaëtan Gilbert (Apr 25 2023 at 11:43):there is harm, it's confusing
Théo Zimmermann (Apr 25 2023 at 11:43):OK, then let's remove the redundant rules.
Théo Zimmermann (Apr 25 2023 at 11:44):But please let's keep the disabled ruleset unchanged for now.
Théo Zimmermann (Apr 25 2023 at 11:44):So that my report is accurate with respect to what we tested.
Gaëtan Gilbert (Apr 25 2023 at 11:44):sure
Théo Zimmermann (Apr 26 2023 at 13:34):It looks like some other people are facing the same issue, so my report is there.
Théo Zimmermann (May 09 2023 at 15:42):Someone answered to my report saying that it looked like the issue had been fixed. I'm on vacation, but someone (e.g., @Gaëtan Gilbert) could test re-enabling the disabled ruleset just before they try merging a PR with coqbot to confirm that this is indeed the case.
Théo Zimmermann (Jun 09 2023 at 13:58):I have just re-enabled the ruleset and it seems to work now.
Théo Zimmermann (Jun 09 2023 at 14:00):So we could delete again the branch protection for master (since it is subsumed by the ruleset).
Théo Zimmermann (Jun 12 2023 at 13:29):Done (legacy branch-protection removed).
Last updated: Nov 29 2023 at 21:01 UTC