Hi Thierry, sure, post issues in the Repo.
Glauco Il giorno giovedì 27 aprile 2023 alle 15:12:58 UTC+2 Thierry Arnoux ha scritto: > Hi Glauco, > > That's excellent news! > > I had a quick try and saw some error messages. We can track that in the > GitHub project issues from here on. > I'm excited to get Yamma to work! > > BR, > _ > Thierry > > On 26/04/2023 20:58, Glauco wrote: > > 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 > > <https://groups.google.com/d/msgid/metamath/7e2db0cb-d8c8-42f6-b3a8-387d13a7127an%40googlegroups.com?utm_medium=email&utm_source=footer> > . > > -- 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/057b5811-cee1-4293-bd91-c1010b5b516an%40googlegroups.com.
