Proposal: Implement "branch protection" on set.mm GitHub repository branch "develop"

33 views
Skip to first unread message

David A. Wheeler

unread,
Aug 24, 2022, 11:17:48 AM8/24/22
to Metamath Mailing List
I propose enabling "branch protection" on our set.mm GitHub repo, branch "develop".

Specifically I propose enabling branch protection with these rules:
* Require a pull request before merging. When enabled, all commits must be made to a non-protected branch and submitted via a pull request before they can be merged into a branch that matches this rule.
* Require status checks to pass before merging. [We] Choose which status checks must pass before branches can be merged into a branch that matches this rule. When enabled, commits must first be pushed to another branch, then merged or pushed directly to a branch that matches this rule after status checks have passed.

This change will mechanically enforce what we're already doing. GitHub will then ensure that every proposed change must be posted as a branch, where people & tools can review before it's accepted.

Rationale: This will help prevent accidentally accepting a change that isn't ready. Mistakes happen, and this will make it less likely that mistakes mess up anything. Enabling branch protection is a widely-applied best practice.

We could also, in the future, mechanically enforce "must be approved by someone else before accepting" if we wanted to. But that's not what I'm proposing at this time.

--- David A. Wheeler

Jim Kingdon

unread,
Aug 24, 2022, 3:56:25 PM8/24/22
to David A. Wheeler, Metamath Mailing List
Sounds good to me. I think requiring a pull request is uncontroversial.

Requiring the tests to pass can sometimes seem like there should be exceptions when the tests fail for reasons which are perceived to not relate to the code being merged, but (1) fortunately our checks have been mostly quite reliable as far as I've noticed on this project, and (2) merging without passing checks can easily lead to situations where checks are failing on develop (and new branches) and that is just unnecessary trouble for pretty much everyone including the person who thought they were saving time by bypassing them.

Benoit

unread,
Aug 24, 2022, 4:23:00 PM8/24/22
to Metamath
Both requirements (requiring a PR and requiring that CI checks pass) sound good to me too.  Like Jim, I was worried about the possibility to waive the second requirement (I think we had a few examples where the PR had to modify the CI checks themselves).  But there probably are ways to do that ?

As for "must be approved by someone else", I think it is wise too, given that there are enough persons allowed to do it.

Benoît

David A. Wheeler

unread,
Aug 24, 2022, 6:03:50 PM8/24/22
to Metamath Mailing List


> On Aug 24, 2022, at 4:22 PM, Benoit <benoit...@gmail.com> wrote:
>
> Both requirements (requiring a PR and requiring that CI checks pass) sound good to me too. Like Jim, I was worried about the possibility to waive the second requirement (I think we had a few examples where the PR had to modify the CI checks themselves). But there probably are ways to do that ?

Yes, indeed there are. Almost all CI check failures happen because there's something wrong with the commit. That's not a surprise, that's what they are for. The two other (less common cases) are infrastructure failure & error in the CI check, which are easily handled:

1. Infrastructure failure. Basically, the tests fail because the CI system crashed. That happened a lot just before we switched from Travis, because Travis' quality of service degraded over time to awful. It's rare on GitHub, they're good at it. Still, if it happens, you can just restart the checks (there's a button to do it), and then accept the updated correct result.
2. Error in CI check itself. In this case, the CI check code is wrong & we need to fix it. In that case, create a new branch to fix the CI check. Once that passes, you can merge it into the "develop" (main) branch, and then merge that result into any failing merged branches.

So yes, there are failure modes, but they aren't hard to deal with. We're basically taking the same approach that millions of software projects use, so we can also build on the way they've fixed its problems.

> As for "must be approved by someone else", I think it is wise too, given that there are enough persons allowed to do it.

I think it'd be a good idea to enforce this automatically too, but let's do that separately.

--- David A. Wheeler

David A. Wheeler

unread,
Aug 25, 2022, 10:16:06 AM8/25/22
to Metamath Mailing List
All: The "set.mm" repository now requires each proposed changes to the primary "develop"
branch to be in a *different* branch, so that the proposal can be reviewed, and can only
be merged if it passes the various checks.

This enforces what we're already doing, and will prevent various accidents.

--- David A. Wheeler

Alexander van der Vekens

unread,
Aug 26, 2022, 12:28:29 PM8/26/22
to Metamath
I am late, but I fully agree. I would also support the "must be approved by someone else".

Reply all
Reply to author
Forward
0 new messages