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/9218034a-a876-9d4a-fee3-c5b33783f0f7%40gmx.net.
