Actually I've reposted this at https://groups.google.com/g/metamath/c/6fQ_GxnPAWI/m/wJ8wzDp3AQAJ; please direct future responses to that thread so we can keep this one to Travis -> GH Actions.
On Fri, Nov 20, 2020 at 3:00 PM Mario Carneiro <[email protected]> wrote: > The plan is to start a new "community verifier" and build it with those > tasks in mind. I think there has been too much fragmentation in verifier > land; this makes it very hard for newcomers, especially those that are not > especially computer literate such as traditional mathematicians. mmj2 is > pretty good, but it's also quite old and the architecture isn't something I > really want to continue to build on. MM1 builds a lot of lean-esque > features into a metamath-like foundation, and I would say as a proof > assistant it's a smashing success, in usability if perhaps not in users. > I've been spoiled by lean to an extent and don't really see current > metamath tools as up to par by comparison, and building mm0-rs has been > enough to convince me that it is feasible to do the same thing for metamath. > > I value metamath's many verifiers; it's a great thing that a new verifier > can be done as an afternoon project. But a proper proof assistant needs a > lot more infrastructure to provide a high quality user experience, and the > community is small enough as it is without additional fragmentation. We've > managed to successfully collaborate on the set.mm github repo, but to > date no verifier has received significant attention from >2 contributors, > except mmj2 which has a couple drive-by contributions beyond the work by > myself and Mel O'Cat (and I'm not actively developing the project anymore). > There is no metamath verifier I would say is in a particularly healthy > state of development. > > As a starting point, I would like to replicate the main functions of > metamath.exe, at least for one-shot tasks. That means reading and verifying > a database, but also parsing it in such a way that edits can be applied, > comments re-wrapped, and semantic information like document structure is > available. Generating the web pages would also be a target. (This is quite > difficult, as metamath.exe is a ball of hacks right now and I would like to > start from a cleaner baseline.) > > For the more advanced tasks, one design question that comes up early is > whether to support "ungrammatical" databases. On the one hand, the metamath > spec considers such databases valid, so they can't be rejected (unless the > database contains the $j command asserting that it is grammatical). On the > other hand, grammaticality enables an asymptotically more efficient > structural storage (trees instead of strings), and also makes it possible > to perform HTML construction in a saner way, where expressions are properly > grouped rather than just appending tokens and hoping it looks well formed > at the end. (This is where a lot of the hacks in metamath.exe come from.) > Note that set.mm and iset.mm are grammatical, as well as most but not all > of the smaller example databases. (I think miu.mm and lof.mm are the main > counterexamples.) Perhaps we can degrade to a simpler verifier-only version > in case the DB is not grammatical. > > As far as language choice goes, I would recommend Rust. Beyond being well > suited for the speed and architectural requirements of a verifier / proof > assistant, both myself and Raph Levien (if I can interest him in this > project) are involved in the rust ecosystem; maybe we can use the Druid UI > framework for the front end. (I want to put in a word of caution though: > one thing I learned from mmj2 is that it's a bad idea to write a text > editor unless that's the main goal. This is not a trivial task and will > suck up all your research time. Outsourcing the editor work for MM1 to > VSCode made so many things easier.) > > But really, the choice is not only up to me, as community buy-in for this > project would be important. The ultimate goal is to become the de-facto > standard proof assistant for metamath, put all our best ideas in it, and > finally get over the popular conception of metamath as not practical for > real mathematicians unless you have a high tolerance for manual labor. > > Mario > > On Fri, Nov 20, 2020 at 9:37 AM Benoit <[email protected]> wrote: > >> 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 >> <https://groups.google.com/d/msgid/metamath/63a8f76e-8d29-4001-b56a-c8812c15f676n%40googlegroups.com?utm_medium=email&utm_source=footer> >> . >> > -- 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/CAFXXJSthR_gDtHCMd6Tsitj-Z3QuWX_6mkHS%3Dv14RBPS%2BptQKw%40mail.gmail.com.
