Mario, do you have some more detail about this project to write (I'm quoting you from github) "a verifier that would satisfy all the constraints of the CI system in terms of capabilities: checking all the typesetting stuff, definition checking, and full verification as efficiently as possible"? Thanks in advance. Benoît
On Thursday, November 19, 2020 at 9:58:15 PM UTC+1 [email protected] wrote: > 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/63a8f76e-8d29-4001-b56a-c8812c15f676n%40googlegroups.com.
