Hi Thierry, You can absolutely try it. I'm now using it in place of mmj2.
I'm using it in linux VMs, but I expect it to work on Windows, too. I don't have a Windows machine with node.js installed, to try it out. If you have node.js installed, you should simply install it from the VS Code marketplace (I hope; with linux it worked out of the box). You open a .mmp , and it activates the extension (it takes a few seconds to parse the main .mm file, see the progress notification on the bottom left) It works better with an additional .mms file, that's a model for "step suggestions" (I'll explain it to the group, when I can). At present, set.mms is a 33 MB text file. You can create it, launching the script /yamma/server/src/stepSuggestion/ModelBuilderScript.ts it takes a couple of hours in my VM. I could probably make it dramatically faster, building parsing trees directly from proofs, rather than running the early parser on every formula of every step of every proof. If someone has a "place" to publish the model, I will send the set.mms.zip file (5Mb size), so everybody can download it. I should add a command to launch the model builder from within Yamma. Full "step derivation" is available a couple of minutes after the .mm is parsed (it is single step, but imho it is really powerful: it infers any kind of statement I've tried, in any proof: even with ten or more parameters, and in long proofs). I hope you'll try it. (DISCLAIMER: while writing formulas, now and then, there's some slowdown because the language server is sending a superlong error diagnostic for every character you type: I will leave this as a "verbose" non default option, but a shorter diagnostic message should fix it) Please, let me know how it goes. Glauco Il giorno mercoledì 26 aprile 2023 alle 09:32:27 UTC+2 Thierry Arnoux ha scritto: > Hi Glauco, > > I have again been away from Metamath for some time, but I see you have > persevered in the development of Yamma. How far are you? > Can now I simply install and use the VSCode extension from the VSCode > Marketplace? > > Thanks, > _ > Thierry > > > -- 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/7e2db0cb-d8c8-42f6-b3a8-387d13a7127an%40googlegroups.com.
