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.
On Sunday, July 30, 2023 at 4:41:31 PM UTC-4 Glauco wrote: > 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 > > > Il giorno domenica 30 luglio 2023 alle 17:45:37 UTC+2 [email protected] > ha scritto: > >> 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? > > -- 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/5b5ba937-dfa2-4b8a-8e1b-4be60df82c6an%40googlegroups.com.
