Yamma

[Antony Bartlett]

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

[Glauco]

I've got it working, thanks :-)

This is cool! (I've never even tried it myself, to clone the repository in a new folder)
Unfortunately, I still feel I'm a newbie about the npm / package.json / tsconfig.json / launch.json architecture, so your support is really welcome.

Please, let me know if / how I could rewrite the installation instructions so that a TS developer would be able to "compile" the "project" :-)

 

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

I've never been able to make LOC_AFTER to work in mmj2 (but for years I've been using a "custom" version, that Mel wrote / maintained for a limited period of time; does LOC_AFTER work in your mmj2 installation?).
I've simplified (I believe) the header structure of .mmp files:
Yamma expects a
$theorem <label>
as a first statement (in the next few days, I plan to feat code to add this line automatically when a ctrl+u is performed; it needs to match the .mmp file name, otherwise a diagnostic / quickFix is displayed)
Now, it is used to check that your theorem is consistent with the database version (if you are refactoring an already existing theorem).
And it will be used to check that the eHyps labels are coherent (<label>.xxx format), otherwise a warning / quickFix is risen (the quickFix can be to either change the label or to add a statement $allowanyhyplabel , that suppresses this kind of warning, for this .mmp file)

Since there's interest, I will add a new statement
$locateafter <label>
(it shouldn't be hard to implement; but it has to be handled both in StepDerivation, in Search statements, and in StepSuggestions)

If you've not tried a Search yet, you can simply invoke it with ctrl + h (same as in mmj2); yamma will analyze the statement under the cursor and populate the search with the most "relevant" symbols (the 3 least frequent ones, if I remember correctly). The "Search Comment:" part is not implemented, yet. And a semantic tokenization for the keywords, is deserved... (near to the top of my current TODO list)

 

Generating a .mmp file from a .mm file is another possible task for me once I am properly armed with a parser.

Absolutely (the same as ctrl+g in mmj2). Thierry already had this feature with its rust language server, metamath-vspa
https://github.com/tirix/metamath-vspa
(Thierry has written a number of impressive theorems and tools!)
This feature is really important, I use it a lot with mmj2, both to refactor proofs for existing theorems, and to write proofs for new, but "similar", theorems.
But I was planning to leave this feature for the second release of yamma (I'm still working on the first one...)
The other "popular" feature that I was planning to leave for the second release, is "renumbering" ( alt + u + r in mmj2)
I understand one expects these features to be there, but I cannot keep adding stuff, otherwise I will never be able to publish something for metamathicians to play with (and give some feedback)

 

Finally, one smaller matter, I notice your unifier puts long terms on a single line (unlike mmj2)

If I'm not mistaken, mmj2 has two/three modes
1. all statements in single line
2. all statements in multiple lines (with standard formatting)
3. "some" statements in multiple lines (with standard formatting)

You can toggle between 1. and 2. using ctrl + o
I'm always in mode 1. (single line) and then, selectively, reformat the single statement I'm focusing on (with right click > "Reformat Step: Swap Alt" ; sometimes, you have to do it twice, to actually work)

Of course, the plan is to port these 3 modes to yamma, too (only mode 1. is available, now)

But now I see what you mean: if you break a statement on multiple lines "by hand", mmj2 keeps your formatting, after a unification. In mmj2 I'm constantly typing ctrl + r to get the "standard" formatting, thus my custom formatting would not survive for long :-)
(as a side note, yamma ctrl+u triggers the "DocumentFormatting" language server protocol standard request, I guess that in my mind it's always been derive/unify/reformat)

Thanks again for having found the time to play with yamma, your feedback is really precious!

Glauco

[David A. Wheeler]

Weird, I never had a problem with LOC_AFTER in mmj2.

A quick workaround in another prover is, if you're trying to prove something,
don't reuse its proof in the database - instead stop reading at that point.
After all, if you're trying to prove "foo", then reusing "foo" seems counterproductive :-).

--- David A. Wheeler

> --
> 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 metamath+u...@googlegroups.com.
> To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/70437437-193e-43ab-b576-9ea758811267n%40googlegroups.com.

[Antony Bartlett]

Just for the sake of clarity:

1.

David wrote:

>Glauco wrote:

>> I've never been able to make LOC_AFTER to work in mmj2 (but for years I've been using a "custom" version, that Mel wrote / maintained for a limited period of time; does LOC_AFTER work in your mmj2 installation?).

>

>Weird, I never had a problem with LOC_AFTER in mmj2

Yes I'm afraid, Glauco, that LOC_AFTER works fine in mmj2 for me too.

2.

Glauco wrote:

> Please, let me know if / how I could rewrite the installation instructions so that a TS developer would be able to "compile" the "project" :-)

Cool, I've got a pull request in with some getting started instructions.  They're just suggestions, don't take any documentation unless you want it (or take it then rearrange to suit you).

https://github.com/glacode/yamma/pull/1

    Best regards,

        Antony

[Glauco]

Cool, I've got a pull request in with some getting started instructions.  They're just suggestions, don't take any documentation unless you want it (or take it then rearrange to suit you).

https://github.com/glacode/yamma/pull/1

Merged, thank you!

Have you tried it in Windows, or Linux?  (I've written yamma in Ubuntu 2016.4 and Ubuntu 2020.4, I've not tried it in Windows, yet)

I'll have to use your instructions myself...   :-)

Glauco

[Antony Bartlett]

On Sun, Dec 25, 2022 at 7:07 PM Glauco <glaform...@gmail.com> wrote:

Have you tried it in Windows, or Linux?  (I've written yamma in Ubuntu 2016.4 and Ubuntu 2020.4, I've not tried it in Windows, yet)

I've tried it on Windows.  As I also use a MacBook for work, I've got a reasonable sense of the differences between shell and command prompt, and the almost exactly-the-sameness of Visual Studio Code on either platform.  As such, I believe the instructions I've given are cross-platform.  However, if developers do run into difficulties running Yamma, I'm afraid they'll just have to let us know,

    Best regards,

        Antony

[Glauco]

I saw your screenshots for the configuration, and it was clear you did those on a c:\... hard drive ; sorry for having asked an obvious question.

Glauco

[Antony Bartlett]

On Sun, Dec 25, 2022 at 8:34 PM Glauco <glaform...@gmail.com> wrote:

I saw your screenshots for the configuration, and it was clear you did those on a c:\... hard drive ; sorry for having asked an obvious question.

Lol, nice deduction, no worries.

Also it was Christmas Day, we were lucky to find each other sober! ;-)

    Best regards,

        Antony

[Thierry Arnoux]

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

[Glauco]

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

[Thierry Arnoux]

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

--
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 metamath+u...@googlegroups.com.

To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/7e2db0cb-d8c8-42f6-b3a8-387d13a7127an%40googlegroups.com.

[Glauco]

Hi Thierry,

sure, post issues in the Repo.

Glauco

[Glauco]

26 april 2023  20:58:45 UTC+2 Glauco wrote:

(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)

I've just published ver.0.0.4 that has a new configuration parameter for the diagnostic message, for theory's formula syntax errors:

  - "short" (default) does not slow down typing

  - "verbose" gives full details about the expected characters and why the theory grammar requires them  (for large grammars, it could slow down typing, since the diagnostic is sent for every character)

Glauco

 

[Glauco]

version 0.0.7 has been published. It supports a

$getproof <label>

statement. This new feature serves as a counterpart to the mmj2 Ctrl+G functionality, allowing you to retrieve specific proofs effortlessly.

A number of bugs have been fixed. Special thanks to @tirix for his precious feedback and contributing to the bug reports.

[Glauco]

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.")

[Glauco]

Yamma 0.0.11 Released (for easier theorem refactoring)

Yamma now builds a (partial) theory, even if some proofs are not valid.

This is a feature that I wish mmj2 had, because it allows for easier change of theorems' signatures.

Here's an example of how it works: in set.mm, ~ liminfgelimsupuz was written for sequences of reals. It had this (3rd) hyp

|- ( ph -> F : Z --> RR )

But it was easy to amend its proof for extended reals. So you can go in set.mm and change its third hyp to

|- ( ph -> F : Z --> RR* )

When Yamma reloads set.mm it will of course create Diagnostics for validation errors, and it will send you a final warning notification (for the whole theory being invalid).

But it will load all the valid theorems, anyway (a valid subtheory)

These are the Diagnostic errors you will get

Theorem liminfgelimsupuz : $e hypothesis doesn't match stack entry. The current hypothesis on the stack is '|- ( ph -> F : Z --> RR* ) . The $e hyp with substitution is |- ( ph -> F : Z --> RR ) .
Theorem climliminflimsup2 : Provable statement liminfgelimsupuz is in the theory, but its verification failed
Theorem climliminflimsup3 : Provable statement liminfgelimsupuz is in the theory, but its verification failed
Theorem climliminflimsup4 : Provable statement climliminflimsup2 is in the theory, but its verification failed
Theorem climliminflimsup4 : Provable statement liminfgelimsupuz is in the theory, but its verification failed
Theorem xlimliminflimsup : Provable statement climliminflimsup3 is in the theory, but its verification failed

You see that you need to fix the proof of liminfgelimsupuz, and then the "immediately" dependent proofs of climliminflimsup2 , climliminflimsup3 and  climliminflimsup4.

xlimliminflimsup is fine because it does not depend immediately on liminfgelimsupuz, thus it does not need any change

Now you can open the liminfgelimsupuz.mmp file and fix its proof, and create the .mmt file.
Then use climliminflimsup2.mmp and climliminflimsup3.mmp to fix their proofs.
Finally, use climliminflimsup4.mmp to fix its proof.

The whole theory will then be valid.

BR
Glauco

[Jim Kingdon]

On November 26, 2023 6:41:32 AM PST, Glauco <glaform...@gmail.com> wrote:
>Yamma now builds a (partial) theory, even if some proofs are not valid.

Ooh nice. I have my workarounds to handle these kinds of changes using mmj2 but having the tool understand it better sounds like it could be a significant help.

[Glauco]

My workaround with mmj2 was (given ~ example to be changed):

- create a ~ exampleNEW (with the new signature)

- search all proofs using ~ example

- load each in mmj2 and change it to use ~ exampleNEW  (then create the .mmt files)

- remove ~ example from the theory and reload the theory

- copy ~ exampleNEW and rename it to ~ example

- load in mmj2 each proof using ~ exampleNEW and change it to use the new ~ example

- remove ~ exampleNEW

I'd like to know if there is a better workflow in mmj2

[Jim Kingdon]

Not that I'm discouraging you from making this better in Yamma but what I do in mmj2 is:

1. Load the file in mmj2 and save .mmp files for everything I want to work on. Quit mmj2.

2. Go to a text editor and make changes to hypotheses or whatever it is.

3. Load the .mmp files. Steps that don't work any more will show an error but you can use mmj2 to help fix those errors (there's a bit of an art to that given how mmj2 handles different kinds of errors but I won't attempt to describe that in full detail here).

What you describe for mmj2 also works, I'm pretty sure I sometimes do that too (for some changes having the old and new both around at the same time can be helpful).

[Glauco]

Yamma 0.0.12 Released:

* Completion items in step suggestions now are not duplicated (when coming from multiple classifiers) and sorted by the Wilson Score (left bound of the 95% confidence interval)

* Removed erroneous empty line in compressed proof formatting (when the parenthesis closing the labels was the last character on its own line)

* Fixed issue with transformation being applied to hypotheses of existing theorems