*>>> you have to know some basic metamath theorems in advance* My goal is exactly opposite :) That's why I designed the interface this way when justifications are not shown by default and users see only statements and if they are proved or not. Apparently this goal is not fully achieved so far due to lack of automation, documentation and examples. But even now it is possible to create proofs without knowing any of the metamath theorems. I even recently provided such a proof (created myself without knowing metamath theorems) as a response here https://groups.google.com/g/metamath/c/f35gd8Cxozo/m/UIwARA0NAQAJ (and I am planning to implement an interface when justifications are easily accessible too :) )
*>>> and often the prove action took very long (several minutes), even after I gave the hint that "6p5lem" can be used.* Usually, when metamath-lamp is given a hint what assertion to use, and other parameters by default, it should work fast enough. Could you please check if you have "parentheses" setting set correctly? In order to do this: 1. Load the database which you encountered this issue with. 2. Go to Settings tab. 3. Click "refresh" button next to the "Parentheses" setting. This will launch a process which will determine what constants are used as parentheses in the loaded database. 4. Click "apply changes" on the Settings tab to save updated parentheses and check if the issue with slow proofs is resolved or not. Parentheses comparison lies in the core of unification algorithm metamath-lamp uses. That's why it may affect performance. If the above doesn't help then I would appreciate if you create an issue in metamath-lamp repository. (please see how to submit an issue at the end of this post) *>>> you have to click A (apply a substitution to all statements), then enter &C1 and 6 manually.* There is a more convenient way to do this which became available only recently. You can use sub-expression selections. This way you can substitute even two or more variables at once. This is demonstrated at 3:40 in this video (no sound) https://drive.google.com/file/d/1IwdHLpQreZ_1CJFZJmptRJc2unO8aNh4/view?t=220 *>>> In the following, a second line with 5 e. NN0 was created (with the massage This statement is the same as the previous one - '2' ) - at first, it was not possible to get rid of it, I succeded, however, after a while...* This kind of error messages is going to appear very often in metamath-lamp. Here is the preferred way of fixing it: 1) Select the statement this error message appeared for by clicking the checkbox left to the statement. This must be the statement right above the error message. And make sure this is the only statement selected. 2) Click "Merge two similar statements" button. This button looks like two lines merging into a single line (like Y). 3) A dialog should appear where you will have possibility to select what statement you want to continue using. (you selected one statement, metamath-lamp finds another duplicated statement automatically) This way one of the duplicated statements will be removed automatically and metamath-lamp will update all the justifications which used the removed statement so they will use the statement you chose to continue using. Also I am planning to automate handling of this kind of situations so in the future it will require less manual work. *>>> I think metamath-lamp is not stable* If you saw any other kind of errors (like errors in the console of a browser), I would appreciate if you submit an issue. If by instability you mean varying speed of work of metamath-lamp, then yes, that might be an issue and I cannot do much about it at the moment, but I will think on how to improve this. Thanks for letting me know this. Thank you for spending your time and providing this feedback. It is very useful for me to understand how others are using this tool and what kind of issues arise. In order to submit an issue in metamath-lamp repository please do the following: 1) Create an issue here https://github.com/expln/metamath-lamp/issues , give it a short name and provide some description of what is not working as you expected. 2) If possible, provide steps to reproduce. I expect it to be not too difficult usually: a) Use "export to JSON" action (located in the top right corner menu on the editor tab) to save json representation of the assistant state at the moment when you are about to reproduce the issue. Attach this json to the issue. b) Specify what next step(s) lead to the issue. 3) Specify the browser name and its version where you face this issue. - Igor On Saturday, May 27, 2023 at 11:50:49 PM UTC+2 David A. Wheeler wrote: > > On Friday, May 26, 2023 at 11:10:02 PM UTC+2 David A. Wheeler wrote: > > > > Ask and ye shall receive!! As of this morning the first draft of the > > metamath-lamp guide is available here: > > https://github.com/expln/metamath-lamp/blob/master/docs/guide.md > > > On May 27, 2023, at 10:17 AM, 'Alexander van der Vekens' via Metamath < > [email protected]> wrote: > > I wanted to proof ( 5 + 7 ) = ; 1 2. > > Ouch, that's a worst case goal for metamath-lamp when compared to mmj2. > The mmj2 tool has automations *specifically* for simple calculations like > this, > while metamath-lamp does not. But it's a valid goal, so carry on! > > > The replacement of a temporary variable is a little bit cumberson: if > you want to replace &C1 by 6, you cannot change it at one place (and then > it is replaced everywhere, as in mmj2), but you have to click A (apply a > substitution to all statements), then enter &C1 and 6 manually. > > In mmj2 you still need to manually replace the work variable (&C1) by its > replacement somewhere (6). > The current assumption in metamath-lamp is that for substitutions you'll > always use the replacement command instead. > > That said, I think you're right, it would be better if metamath-lamp also > allowed people to > just edit a work variable into an expression and have unify automatically > do the replacement. > I've added that as a proposal here: > > https://github.com/expln/metamath-lamp/issues/43 > > > In the following, a second line with 5 e. NN0 was created (with the > massage This statement is the same as the previous one - '2' ) - at first, > it was not possible to get rid of it, I succeded, however, after a while... > > You should be able to select the statement & then choose "delete". If that > didn't work, I'd love to know why. > > > At the end, I needed about one hour to finish the proof successfully > (with metamath.exe it was done within a few minutes). > > To summarize, I think metamath-lamp is not stable/intuitive enough to be > suitable for a beginner at the moment. > > > > Finally, it would be very helpful if screen shots were available in this > user guide. > > Good point. In the long term I intend to create a video, just like I did > with mmj2, > but screen shots are still a good idea. > > Thanks for the feedback! I think you're right that metamath-lamp needs > improvements > in its UI & capabilities. However, I think some of that suggests a need to > improve its documentation > to clarify how to use it; mmj2 also has some oddities that work fine once > you know what they are. > I'm going to work on improving its documentation to hopefully make it > easier. > > I still think it is helpful to have at least one tool that work "without > an install" and can > immediately work on smartphones. > mmj2's automations and some specific mechanisms give it power that > metamath-lamp > currently lacks, but some people may be unwilling to go through the effort > of installing a tool > just to try it out. I'm hoping that metamath-lamp can be, at the least, a > way > to entice people into trying to create metamath proofs themselves. > > --- 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 [email protected]. To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/d1c27ad0-4cad-406b-9b12-ccd112f8fcc3n%40googlegroups.com.
