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/CAJ48g%2BC6h-K1dpWuijQ2mw2B%3DHSwBV%3DOgwCc38Waikq4hP-FHQ%40mail.gmail.com.
