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/6BA43F15-6640-428A-84E0-1AE795C8A392%40gmx.net.
