Hi Thierry, thanks for this useful thread.
As Benoit wrote, I would have also preferred everyone to work on mmj2. But when I myself tried to contribute, I always run into some dependency / "java version" issue. When it became clear that a Language Server was the way to go, I settled on TypeScript for a number of reasons: - I would have not been able to contribute to the Rust project, because I didn't have a good enough theoretical background: I've always been kind of a "mmj2 user", it simply was a tool for me to write bulletproof proofs (I once read an "old" version of the Metamath book, but back then I was a complete newbie and I didn't get lots of details) - now that I've written my own parsers, verifiers, generator for theory specific grammars, unifiers (well... still working out this last one...) I can at least understand what you are doing with metamath-knife :-) - my first attempt was with dotnet (the framework I prefer), and the parser / verifier was pretty good and fast, but as soon as I tried to work on the Language Server, as always, I stumbled against version conflicts between the Language Server SDKs I found on examples and the current dotnet version - then I checked the list of existing Language Server Implementations https://microsoft.github.io/language-server-protocol/implementors/servers/ and (if I remember well) there were 49 TypeScript implementations, (dotnet was the second most popular) and 3 Rust implementations Then I looked at the LSP SDKs: https://microsoft.github.io/language-server-protocol/implementors/sdks/ If you compare the TypeScript LSP SDK https://github.com/Microsoft/vscode-languageserver-node to the SDKs for the other platforms, you get an idea of how well maintained the TypeScript LSP SDK is. And the TypeScript's SDK is used (for examples) in the LSP spec - I did not want additional dependencies. If you use VSCode, you already have Node.js installed, and you don't need to install (the right version of) anything else. When I tried Thierry's metamath-vspa (it's supercool!) I immediately run into a RUST language server version issue (I'm sure the final version will not have this kind of problems, for the final user; but for contributors I guess it will always be a problem) I'm not sure TypeScript will have the speed needed to be a smart enough Proof Assistant. If my little LS settles down, I'll be more than happy to share ideas / features with the Rust LS Repo and contribute to the Community Verifier (as I wrote, now I have a better understanding of the underlying framework). The flip side, is that in the last few months I had no more time to spend on new proofs and my mmj2 muscle memory is a bit rusty. I hope it pays out in the long run. BR 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/e004d1ef-0c4e-43c1-9954-70d83e1cc0een%40googlegroups.com.
