On Sat, Nov 21, 2020 at 6:09 PM 'ML' via Metamath <[email protected]> wrote:
> 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? > As I mention in the other post, I think it is most likely to share more code with mm0-rs than a pure verifier like smm3, although it's possible we can remix some of the ideas from that. There are a lot of cool tricks in that program that power its best in class running time, but optimized string substitution doesn't translate well to a robust proof assistant, where you want to manipulate the data in a lot of ways beyond simple unification. Probably we should just leave smm3 as is and use a more expression based representation for terms. Writing a verifier from scratch is not really a problem. It's everything else that is difficult. > 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. > If there is enough interest from others that I'm not the only one on the project, I don't mind taking the lead here. If it incorporates common code from mm0-rs then that will be a good excuse for me to split it off to a new project (the MM0 monorepo is getting pretty hefty) and maybe also expose a library (depending on whether this new verifier is literally mm0-rs under some settings or a separate executable that just links against a library with common code from mm0-rs). That said, I am nearing the end of my PhD and probably shouldn't be devoting large quantities of time to something that doesn't move my thesis forward. :P 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/CAFXXJStwFp05zptsfD7w5Dq1a-VixsMG-6ozz455PtUf2yLzvg%40mail.gmail.com.
