> 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 any case, let’s get the jobs migrated first. We can then discuss if it’s worth trying to have a separate “nightly”. --- 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/642D3F04-A010-4B01-A365-0469C7430DB9%40dwheeler.com.
