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 On Monday, July 31, 2023 at 12:10:25 PM UTC+2 Glauco wrote: > 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 [email protected] > 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? > > -- 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/1989155f-69ed-4096-b51d-a40d8b93206cn%40googlegroups.com.
