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 > On Aug 24, 2022, at 6:03 PM, David A. Wheeler <[email protected]> wrote: > > > >> On Aug 24, 2022, at 4:22 PM, Benoit <[email protected]> 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 -- You received this message because you are subscribed to the Google Groups "Metamath" group. To unsubscribe from this group and stop receiving emails from it, send an email to [email protected]. To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/413271C0-BFBB-486C-A34E-2987E4961348%40dwheeler.com.
