Can anyone tell me where to find an explanation of the .mmp format?

[Marshall Stoner]

I'm working on my own database not set.mm.  I just installed yamma because I want to work in vscode, but I don't get it.  It tells me to load a .mmp file but where do you even get such a file?  I name a file with .mmp extension but it just brings up an empty text file.  There is no help on how the mmp format works.  Is there any way to load an already completed proof from the .mm file?

[Glauco]

Hi Marshall,

.mmp is the format used by mmj2 (I've never found a formal bnf for its syntax)

Yamma uses a slight variation of that format (the header is different and yamma allows some commands, in the text)

- save set.mm in a folder

- in VSCode, open that folder (with ctrl+k+O)

- open/create an empty test.mmp file

- by default, Yamma looks for set.mm in that folder. It takes about 10 seconds to parse/verify everything (an information messagebox in the lower right corner tells you if everything is fine)

- type ctrl+space (the usual command to get suggestions)

- since your test.mmp file is empty, there will be just two suggestions:

$theorem

$getproof

- select $getproof

- Yamma will then show you a list of autocompletion with ALL the proof labels in set.mm

- select, for instance 0bits  (in alphabetical order it is almost at the top of the list)

- yamma will read 0bits' proof, and it will translate it in .mmp format.

And you are good to go!

Please feel free to ask questions (Thierry is probably using Yamma more than I am; at present I'm more focused on improving the extension, rather than on using it).

Glauco

[Marshall Stoner]

Are you saying it won't recognize a file not called set.mm?  Lamp works on any database, but it doesn't have any option to load a proof from the database.  There are meta-theorems that can be proved recursively, but for specific instance I can construct the next higher one in the chain by loading the previous proof and substituting a new expression.  Typing everything in is tedious.  Also, the matching diagram with Lamp is a really cool learning tool, but you have to write in your own proof to see it.  You can't quickly load up a copy of an already existing proof.

[Glauco]

set.mm (in the current folder) is just the default.

You can use any .mm file you wish:

- enter VSCode settings   ctrl+,

- Extensions > Yamma

- set 'Mm File Full Path' to your .mm file   (mine is set to /mnt/mmt/set.mm   )

Glauco

p.s.

disclaimer: Yamma has mainly been 'tested' on set.mm and subtheories of set.mm

Il giorno domenica 30 luglio 2023 alle 23:58:38 UTC+2 mbsto...@gmail.com ha scritto:

Are you saying it won't recognize a file not called set.mm?  Lamp works on any database, but it doesn't have any option to load a proof from the database. roof from the .mm file?

[Igor Ieskov]

Hi Marshall,

Thank you for your feedback on mm-lamp!

The ability to load an existing proof from the database will be available in the next version of mm-lamp. However, it is already available in the "dev" version https://expln.github.io/lamp/dev/index.html

If you use this feature in the dev version and find bugs, please feel free to report them in this issue on GitHub https://github.com/expln/metamath-lamp/issues/8

Here is an instruction how to load an existing proof:
1. Open the Explorer tab and find a theorem.
2. Click the theorem name, so it opens in a new tab.
3. In that new tab, open the "hamburger" menu and select "Load this proof to the editor". This will open a dialog window.
4. The dialog window shows two parameters:
"Adjust the context" - If this parameter is checked then mm-lamp will change the context to include everything up to the theorem but not more. If this parameter is unchecked then the context will not be changed.
"Load proof steps" - If this parameter is checked then mm-lamp will load all the steps of the proof. If this parameter is unchecked then mm-lamp will not load intermediate proof steps; only hypothesis steps and the goal step will be loaded. This may be used to try to prove an existing theorem from the scratch for learning purposes.
5. Select/unselect these two parameters depending on your needs and click the "Load" button. The proof should be loaded in the editor tab.

-
Igor