> 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/99B126E7-55F6-4BA1-B63E-5FD6F15D4EDD%40dwheeler.com.
