Hi Mario, here https://groups.google.com/g/metamath/c/raGj9fO6U2I/m/2tQseJ3CBwAJ you show peano.mm1 in VSCode and you write "The basic idea is that MM1 is a scripting language for assembling MM0 proofs and statements. It's untrusted, and functions as the IDE for MM0"
Looking at one of your presentations I've seen you've also completely translated set.mm to mm0, isn't it? Would it be possible, for you, to video-record a session in which you proof a simple new theorem (starting from the mm0 translation of set.mm) ? No audio is needed, and there's no need to make the video available on youtube to everybody. Just a short session to show us how it would be the workflow: load available axioms/definitions/terms/theorems > create new theorem> write/verify proof > save created proof (add to the pre-existing "stuff") Glauco Il giorno domenica 22 novembre 2020 alle 23:03:13 UTC+1 [email protected] ha scritto: > On Sun, Nov 22, 2020 at 12:39 PM Glauco <[email protected]> wrote: > >> Please, let me know what's the best environment to set up to contribute >> to the new tool: >> >> - VSCode + RUST seems to be the candidate, right? (if it were possible to >> have a portable environment it would be a plus) >> >> - at least Windows + Linux is a must, I guess >> > > Note that Visual Studio Code is an open source editor platform by > microsoft available on all operating systems. It has no relation to Visual > Studio, which is a bloated proprietary piece of crap. I guess they liked > the name. > > Also, mm0-rs uses a standard called the "language server protocol" to > communicate to VSCode, which is specifically intended to address the > problem of many languages supporting many editors. In theory, any editor > which supports LSP (which I believe includes most of the big ones at this > point - vim and emacs for sure, haven't seen whether eclipse supports it > yet but I wouldn't be surprised) can run any LSP-supporting language > server. LSP is mostly pushed by microsoft so it probably has best support > in vscode, though, and also I have only tested mm0-rs with vscode because I > use it daily, but if someone is interested to maintain support for their > preferred editor we can probably make it happen. > > -- 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/371e58ed-5f9e-470b-bab4-e80d355e0e9an%40googlegroups.com.
