On Thu, Nov 19, 2020 at 3:41 PM David A. Wheeler <[email protected]> wrote:
> > > On Nov 19, 2020, at 3:26 PM, Mario Carneiro <[email protected]> wrote: > > 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. > > Some verifiers check not only for the proof, but for certain conventions > that we use. > If there *is* a disagreement, it’s useful to know as soon as possible. > In my vision for the CI verifier, it checks everything that CI currently checks: line lengths, style, htmldef entities, $j commands, comment parsing, definition checking, etc in addition to being a plain old verifier. So if *any* nightly verifier reports an error that CI missed then there is a bug in the verifier suite somewhere, not in the input files. 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/CAFXXJStcoNmfgoeade%3DOyaMhFW7zopX-PHk-rSs1p9NY0gY%2BWg%40mail.gmail.com.
