Normally I'd be more conservative about starting from scratch vs improving the existing tools, but MMJ2 is very broken, so I'd be willing to participate in a rewrite.
(I'd like to mention that MMJ2 being this broken is partly Java's fault, for no longer being careful about backwards compatibility. Undo/redo is broken since Java 9, and as far as I can tell it would need to be reimplemented completely, because a Swing feature it relied on was removed. All the macros will also be broken eventually, because the Nashorn engine, which they rely on, has been removed in Java 15. And I suspect there's more examples of this.) Still, much like how it's better to outsource text editing to an existing editor, it's better not to start from scratch if we can help it. So if Rust is really the language we decide to use, I'd recommend building off of the existing Rust verifier if possible. I assume that https://github.com/sorear/smetamath-rs is the Rust verifier that's been mentioned? --- Improving Metamath tooling is something I definitely want to do. I was already working a towards improving MMJ2, in my personal fork I fixed all the linter warnings, ported some of the old batch file unit tests, and also started porting the macros to use the Rhino javascript engine (in preparation for Nashorn's removal). No one seems to be explicitly saying that they will start this project. I'm not sure I can take the lead, because I don't know much yet about how to implement a proof assistant, and because this is meant to be a community project but I haven't participated much in the community. Still, I've used Rust before, and as a first step, I could try to translate MMJ2's LRParser to smetamath-rs, and report on my progress here in a few weeks. On Friday, November 20, 2020 at 3:02:44 PM UTC-5 [email protected] wrote: > 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/df214732-89df-4495-a07c-8e5418322894n%40googlegroups.com.
