I believe mmj2 is good as an IDE and with a couple of improvements it would even "n x." boost my speed in writing proofs (intellisense when proving backward, being the most important missing feature).
I've tried a couple of times to set up Eclipse for mmj2, but got stuck when trying to stepdebug the code after a ctrl+u: a few threads are thrown and the debugger doesn't "attach" to at least one of them. I'm sure it depends on having the right Java / Eclipse environment, but I love to write proofs, so I've never even asked Mario / David any help about setting up the right "environment" in order to help with the mmj2 development. I'm currently using a Mel O'Cat release that's not available anymore online, because he improved the search page in that release. I believe it's good enough to write long and complex proof. I've always been of the opinion that the most effective strategy would have been to improve mmj2, rather than starting new projects. I'd be really excited If we can come up with a better PA. I don't know anything about RUST, but I'm confident I can learn it. I hope we will set up a well-defined/isolated IDE: IMHO, the biggest problem with mmj2 is that it depends too heavily on the jvm version, the Eclipse version, the Eclipse project version. Recently, I tried to download the current mmj2 version but I wasn't able to run it, neither in Win10, nor in Ubuntu. I got runtime errors probably due to jvm version conflicts. I'm sure I could have fixed them, but I gave up and went back to my Mel O'Cat "special edition" :-) Consider that I spend hours every day in mmj2, I can't imagine a newcomer facing this kind of problems. I completely agree with the "don't build the text editor" approach. I hope we can work on this new PA together. My main concern is that it will take a long time before being comparable to mmj2 and until then nobody will use it for "real" work and this will slow down its development. Glauco Il giorno venerdì 20 novembre 2020 alle 21:02:44 UTC+1 [email protected] ha scritto: > 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/cdbffce6-df3a-4ffe-bd80-62982d4e7674n%40googlegroups.com.
