Stream: Coq devs & plugin devs

Topic: Branch rulesets


view this post on Zulip 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.

view this post on Zulip Gaëtan Gilbert (Apr 19 2023 at 19:43):

cool

view this post on Zulip 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?

view this post on Zulip 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.")

view this post on Zulip 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?)

view this post on Zulip Jason Gross (Apr 19 2023 at 23:32):

Should https://github.com/coq/coq/rules/3041 apply to release branches and not just master?

view this post on Zulip Jason Gross (Apr 19 2023 at 23:32):

Should there be rulesets about tag creation?

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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).

view this post on Zulip 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).

view this post on Zulip Théo Zimmermann (Apr 20 2023 at 08:34):

There is one: https://github.com/coq/coq/rules/3016

view this post on Zulip Théo Zimmermann (Apr 20 2023 at 08:34):

Thanks a lot for all the feedback!

view this post on Zulip 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)

view this post on Zulip Théo Zimmermann (Apr 21 2023 at 07:18):

Indeed, good idea. I'll add a rule for this.

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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)")?

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Gaëtan Gilbert (Apr 25 2023 at 11:28):

that didn't work, reverting

view this post on Zulip 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

view this post on Zulip Gaëtan Gilbert (Apr 25 2023 at 11:31):

ok that worked

view this post on Zulip 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.

view this post on Zulip Théo Zimmermann (Apr 25 2023 at 11:43):

Thanks for testing this. I will report the bug to GitHub's staff.

view this post on Zulip Gaëtan Gilbert (Apr 25 2023 at 11:43):

there is harm, it's confusing

view this post on Zulip Théo Zimmermann (Apr 25 2023 at 11:43):

OK, then let's remove the redundant rules.

view this post on Zulip Théo Zimmermann (Apr 25 2023 at 11:44):

But please let's keep the disabled ruleset unchanged for now.

view this post on Zulip Théo Zimmermann (Apr 25 2023 at 11:44):

So that my report is accurate with respect to what we tested.

view this post on Zulip Gaëtan Gilbert (Apr 25 2023 at 11:44):

sure

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Théo Zimmermann (Jun 09 2023 at 13:58):

I have just re-enabled the ruleset and it seems to work now.

view this post on Zulip 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).

view this post on Zulip Théo Zimmermann (Jun 12 2023 at 13:29):

Done (legacy branch-protection removed).


Last updated: May 18 2024 at 10:02 UTC