Without writing a new verifier, the cheap way to obtain this is to run the minimal subset of existing verifiers sufficient to get all these auxiliary checks: I believe metamath.exe and mmj2 should be sufficient, although mm-scala does some $j checking beyond mmj2 so it might also have to be included. But ultimately I would like to have all of this in one verifier because it's faster and it would also make a good foundation for the next generation proof assistant if it is able to have a solid semantic understanding of metamath files. (Imagine if renaming could be done correctly without relying on grep!) I've been doing a significant amount of work on mm0-rs to turn it into just such a program for MM1, and it is nice to be able to have all the niceties of a normal programming language IDE like go to definition, find references and rename in addition to proof assistant like features. I'm not sure I want to go back to mmj2 at this rate.
On Thu, Nov 19, 2020 at 3:46 PM Mario Carneiro <[email protected]> wrote: > > > 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/CAFXXJSv7t3QOj-J3M5_AbXgVciS1ReqOqU25FRc3fiDPvt128Q%40mail.gmail.com.
