Relocated from https://groups.google.com/g/metamath/c/NMZA_JRkU4U/m/ccP9bXZlAQAJ:
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 > 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. -- 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/CAFXXJSv5mf9e3mQzhEUTJi8dP9ct7dha9bEGP2zwjg4W9QKFtA%40mail.gmail.com.
