Is there a formal spec for the mmp format? An EBNF like what we can find in Appendix E (of the Metamath book) for the mm spec?
I've a Typescript parser/verifier for .mm/.mmp files that's working pretty well, but I'm adding new features, and I would like to standardize the names of Classes/Properties/Methods to an "official" spec. If a BNF is not available, is there a "standard" name for the "blob" at the beginning of any mmp statement, I mean, this guy here 72:71,70:mpbid (I've looked at some mmj2 source code, but I've not been able to easily find a place where that blob is referenced with a name) Thanks in advance Glauco Il giorno martedì 15 febbraio 2022 alle 03:40:33 UTC+1 Thierry Arnoux ha scritto: > Hi Glauco, > > MMJ2-style unification is certainly a goal! Many building blocks for this > are actually already in place - not all, but we’re slowly getting there. > > An even more remote goal would be to use this framework to build a more > tactics-based proof assistant, but that’s in a much more distant future! > > Right now Metamath-knife’s API is still changing (and I expect it to > continue). One thing you’ll have to take care about if building > metamath-vspa is to use the correct version. I hope we fix that soon. > > Any help is certainly welcome! The choice of Rust was discussed in this > forum a while ago, one motivation being that Ralph and Mario both master > it. I’ve been self-learning Rust, I still am not very good and I certainly > still have a lot to learn, but I had a lot of fun learning it. It has a lot > of features I was hoping for when programming in C. > > Each editor function (diagnostics, completion, references, search, > formatting, etc.) is a different functionality which can be built in > parallel and stay relatively independent, so it shall be very feasible to > have several people working together on that project. > > BR, > _ > Thierry > > > > Le 15 févr. 2022 à 03:54, Glauco <[email protected]> a écrit : > > > > Thierry, this is so cool! > > > > Is a mmj2 ctrl+u like action available? Please, feel free to ask if you > need help with this one (I don't know anything about Rust, but it's now on > top of my list of things to learn) > > > > Can't wait to build and try it! > > > > Glauco > > > > -- 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/7e84b4c0-e4f4-409b-b54d-4d51f4edaf74n%40googlegroups.com.
