On Thu, Nov 19, 2020 at 1:47 AM Jim Kingdon <[email protected]> wrote:
> All sounds good, thanks for looking into this. > > I'd say that running everything on every pull request would be my > preference, and I don't think it takes that long to run (at least, it > hasn't on travis). Nightly is an option if we have to, but if the > nightly run fails there is a debugging step of figuring out which of the > pull requests merged that day caused the problem. > If a nightly run fails, then that means there is a buggy verifier, and today's test sussed it out. It doesn't really matter what happened that day in set.mm, because the CI verifier should catch any errors in the relevant commit. There are two possibilities: * One of the large list of nightly verifiers is buggy and is spuriously failing on the correct set.mm of that day. In that case we should contact the author, try to get it fixed, and probably remove it from the list of nightly verifiers until it is fixed. * The CI verifier is buggy and failed to catch a problem that was introduced some time that day in set.mm, and the nightly verifiers (probably almost all of them) are flagging it. This is also not too hard to localize, because at least some of the verifiers have good error reporting and will point at the particular proof that is going wrong. In any case, this isn't something where we need to chase the set.mm commit, because it doesn't matter - we've just generated a new test case for the verifier, so we should fix the CI verifier, get it passing or failing properly on the new info, and then fix set.mm if it turns out to be broken. This is why I say that the nightlies are really a test case for the verifiers - under no situation is the blame laid on the commit that pushed a bad proof, because disagreement between verifiers is always a verifier bug. All the per-commit blame for bad proofs is delivered by the CI verifier that runs on every commit. Mario -- 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/CAFXXJSvwvs5Jc-nCu72Wa_MbwaMXVGD2ryRYUeupG3JNXqchzA%40mail.gmail.com.
