Version 0.0.10 has been published: you can now create a model for step suggestions directly within the extension, eliminating the need for external scripts.
The usual VSCode progress notification will keep you informed throughout the process, which typically takes about an hour on a slow VM. (To create the model, open an .mmp file, and then press Ctrl+Shift+P and type "Create Model" or right-click and select "Create Model.") Il giorno venerdì 23 dicembre 2022 alle 13:53:01 UTC+1 [email protected] ha scritto: > Glauco wrote: > > Antony wrote: > >>I'm still hoping I can figure out how to use Glauco's parser, but I > realise I've been frittering away my spare time writing docker containers > full of metamath command line tools, and working through David A Wheeler's > video in mmj2 and yamma as Glauco recommended, instead. However, I do > intend to be back on the parse issue that's perhaps become a bit of a > blocker for both of us, soon. > > Hi Antony, feel free to open issues in the yamma repository, I'll be > more than happy to help you to try a "Run Client" session :-) > > I've got it working, thanks :-) > > mmj2's great, I really like the unifier. As a text editor... well I'm > thrilled you're porting the core functionality to Visual Studio Code (VSC) > - an integrated development environment that I, and probably literally > millions of other developers use every work day (74% of respondents in the > 2022 StackOverflow developers survey use it). I think you've underplayed > the significance of your project Yamma, and it's going to become a major > factor in metamath's near future ("near" from the perspective of a project > that started in 1992, at any rate). Of course to capture the biggest > audience for metamath we would also want tools to run in people's browsers > including on their mobile phones, and the fact you're targeting the > JavaScript platform is also a good step in that direction (even while it's > more Samuel and I that have our eyes on that target). > > Glauco wrote: > > it's clearly not yet ready for prime time > > The biggest obstacle to me following David's video in yamma is that the > LOC_AFTER feature of a .mmp file doesn't seem to be working yet. So it > keeps trying to unify and prove reccot from reccot, which is cute and > amusing but not very practical. I assume you would have fixed this by now > if it was easy, so I plan to work around it with a simple command line tool > for truncating a .mm file once I am comfortable with your parser. I > realise that's become something of a mantra for me, there are at least four > things I plan on doing once I am comfortable with your parser. Fortunately > I will have run out of displacement activities once I hit 'send' on this > email ;-) Generating a .mmp file from a .mm file is another possible task > for me once I am properly armed with a parser. (getting a working demo of > it streaming is the only item not relevant to the present discussion). > > Finally, one smaller matter, I notice your unifier puts long terms on a > single line (unlike mmj2), and suggest the best way for us npm users to > sort that out is with a prettier plugin. I've already got one for .mm > files: > > https://github.com/Antony74/prettier-plugin-mm > > It's based off of the checkmm verifier which I haven't bothered to switch > off. As such it will on prettify verifiable .mm files, whereas ideally we > want it to prettify any parsable .mm or .mmp file. I'm planning to do the > relevant rewrite "once I am comfortable with your parser" ;-) > > Hope the feedback I've given is helpful (even though I don't seem to be > able to shut up about parsers). > > Best regards, > > Antony > > > > > -- 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/a5d3087a-95f5-4e12-88db-11d1c14e3e86n%40googlegroups.com.
