mm-lamp v10 <https://expln.github.io/lamp/v10/index.html> is released with few new features:
1. Autocompletion for parentheses - when you type an opening parenthesis followed by a space then the closing parenthesis is added automatically and the cursor is placed in between those parentheses. 2. Syntax validation and “syntax aware” selection. 3. Graphical visualization of justifications. The below demo almost repeats the proof from the v1 demo but using the new features this time: https://drive.google.com/file/d/1IwdHLpQreZ_1CJFZJmptRJc2unO8aNh4/view?usp=sharing Best regards, Igor On Tuesday, April 25, 2023 at 12:31:04 AM UTC+2 Igor Ieskov wrote: > Hi all, > > I have implemented a few new features in the version 9 of mm-lamp > https://expln.github.io/lamp/v9/index.html : > > > 1. > > Reading the set.mm file from us.metamath.org. > 2. > > Possibility to share editor state via URL and JSON. > 3. > > Possibility to add a description with basic formatting. > 4. > > Showing a proof table for the proof being exported. > > > Here is a short demo (without sound) > https://drive.google.com/file/d/1sM19TfF-7nRfhnnsKA_i_1I0H18mUyX5/view > > > A few comments on the new features: > > > 1. > > Reading the set.mm file from us.metamath.org. This is configurable, > other URLs may be added on the settings tab. When an editor state is > exported, if all the loaded mm files are loaded from the Web then they > will > be automatically reloaded when this state gets imported. For each URL a > user is asked if they want to load data from that URL. The user has the > possibility to mark some URLs as “trusted” then data will be loaded from > such URLs without asking. This is also configurable on the settings tab. > 2. > > Possibility to share editor state via URL and JSON. Such URLs contain > a Base64 encoded editor state. It may be decoded with many online Base64 > decoders if for some reason a URL is not opened by mm-lamp but it is > needed > to see its content. GitHub IO limits URL length so that only about 5K > characters in the editor state may be shared via URLs without problems. > Exporting/Importing to/from json doesn’t have this limitation. > 3. > > Possibility to add a description with basic formatting. Initially I > planned to use some existing advanced component which is capable of > rendering markdown. But then I realized that I don’t control what is > injected into the page which makes XSS attacks possible. So I ended up > implementing my own markup language which produces simple html without the > risk of XSS attacks (at least I think so, if anyone finds such a > possibility, please let me know). As a downside, formatting is very basic. > But I can add new formatting features if needed. > > > > And one more note. The previous version of /latest/index.html page > truncated a query string when redirecting to the actual latest version > page. That made redirection with the editor state in the URL impossible. I > updated that page (added a programmatic redirection). But a browser may > cache the old version. So, if opening a URL with an encoded editor state > doesn’t load that state, probably clearing of the cache will help. > > > This is the link from the demo - proof > <https://expln.github.io/lamp/latest/index.html?editorState=eyJzcmNzIjpbeyJ0eXAiOiJXZWIiLCJmaWxlTmFtZSI6IiIsInVybCI6Imh0dHBzOi8vdXMubWV0YW1hdGgub3JnL21ldGFtYXRoL3NldC5tbSIsInJlYWRJbnN0ciI6IlJlYWRBbGwiLCJsYWJlbCI6IiJ9XSwiZGVzY3IiOiJBIHNpbXBsZSA8YSBmb250LXdlaWdodD1cImJvbGRcIiBjb2xvcj1cImdyZWVuXCIgaHJlZj1cImh0dHBzOi8vdXMubWV0YW1hdGgub3JnXCI-TWV0YW1hdGg8L2E-IHByb29mLiIsInZhcnNUZXh0IjoiIiwiZGlzalRleHQiOiIiLCJzdG10cyI6W3sibGFiZWwiOiI0IiwidHlwIjoicCIsImNvbnQiOiJ8LSAoIDMgKyAyICkgPSA1IiwianN0ZlRleHQiOiI6IDNwMmU1In0seyJsYWJlbCI6IjMiLCJ0eXAiOiJwIiwiY29udCI6InwtIDIgZS4gQ0MiLCJqc3RmVGV4dCI6IjogMmNuIn0seyJsYWJlbCI6IjIiLCJ0eXAiOiJwIiwiY29udCI6InwtIDMgZS4gQ0MiLCJqc3RmVGV4dCI6IjogM2NuIn0seyJsYWJlbCI6IjEiLCJ0eXAiOiJwIiwiY29udCI6InwtICggMiArIDMgKSA9IDUiLCJqc3RmVGV4dCI6IjIgMyA0IDogYWRkY29tbGkifV19> > > > > - > > Igor > > > On Monday, April 10, 2023 at 5:38:13 PM UTC+2 Igor Ieskov wrote: > >> Hi all, >> >> I have released version 7 of metamath-lamp with bug fixes and a few new >> features. >> >> https://expln.github.io/lamp/v7/index.html >> >> Here is a demo >> https://drive.google.com/file/d/1haJff_AN1M6HZGrWXsgqzrxq-Di84gmZ/view >> >> I used the text-to-speech function of my video editor to add voice >> explanations in the demo. It might sound a bit unusual, but believe me this >> is much better than listening to what I retrieve when recording my own >> voice. >> >> In the demo I used the “my-editor-state.json” set of statements provided >> by Thierry in one of the posts above (on Jan 11 2023, if anyone wants to >> find it quickly). >> >> Thank you Thierry for providing “my-editor-state.json”. It allowed me to >> discover some use cases I was not aware of before and helped me a lot in >> improving mm-lamp. I also saved it in the source code and implemented a few >> tests based on it - >> https://github.com/expln/metamath-lamp/blob/4b25515acb8174086cd970d1b10cc4a26821dbba/src/metamath/test/resources/int-test-data/restore-missing-disjoints/editor-initial-state.json >> >> Few things I want to mention: >> - I edited the demo video and cut out some long running phases of >> unification and bottom-up proving for the demo to be shorter. So in reality >> mm-lamp might be slower. >> - While recording the demo I realized that exporting local variables >> (this is a new feature explained at the end of the demo) might not work >> well if such variables are not used explicitly in the statement being >> exported or its hypotheses but are used in its proof. I have not tried to >> reproduce this bug but I see in the code that this may happen. I am going >> to fix this in a future version. >> - I forgot to update some tooltips with hotkeys. Here are the correct >> hotkeys: 1) to start editing a statement, variables or disjoints - left >> click it; 2) to save the changes - press Enter; 3) to start a new line in >> variables or disjoints text fields - press Shift Enter. >> >> If anyone sees any mistakes in the current design or finds any issues or >> bugs, please feel free to let me know. Any feedback is appreciated. For >> issues and bugs it’s probably better to use the “Issues” section of the >> repository https://github.com/expln/metamath-lamp/issues >> >> David, I walked through the mmj2 tutorial. Please find some my thoughts >> below: >> >> 1) currently mm-lamp doesn’t allow adding comments. I am going to >> implement this. >> >> 2) undo/redo is also not supported in mm-lamp. Most probably I will not >> be able to implement this feature by storing the editor state in the URL as >> you mentioned because internal representation of the editor state is >> actually more than we may see in the local storage. I could store editor >> states to the local storage after each modification (I mean keeping all >> previous versions of editor states). But then I am limited by the available >> amount of the local storage which is usually not too big. I keep thinking >> on how I can implement this feature. >> >> 3) mmj2 can keep few identical statements and mm-lamp cannot. I cannot >> change this because this lies in the core - it allows me to simplify some >> parts of the code. Please let me know if this is a vital or very handy part >> of creating proofs. If it is needed to keep few possible proofs for a >> single statement then I will try to implement multiple justifications for a >> single statement. >> >> 4) Renumbering of statements, loading existing proofs - I am going to >> implement this. >> >> 5) mm-lamp cannot automatically prove “|- ( ; 9 5 + 1 ) = ; 9 6”. I hope >> this will be resolved once I start adding heuristics. >> >> 6) Search capabilities of mmj2 are profound, I need some time to learn >> this and figure out what I can steal. >> >> Best regards, >> Igor >> >> >> >> On Tuesday, February 14, 2023 at 12:14:18 AM UTC+1 Igor Ieskov wrote: >> >>> >>> *>One broad suggestion: Could you give it a short & less generic >>> name,>since there are other Metamath proof assistants?* >>> >>> That’s done! The new name is metamath-lamp “Lite Assistant for Metamath >>> Proofs”. >>> I renamed the repository accordingly: >>> https://github.com/expln/metamath-lamp >>> I guess I need to create a pull request to make corresponding changes on >>> https://us.metamath.org/other.html ? I will try after sending this >>> email. >>> >>> >>> >>> >>> *> You might want to include, on the screen or an "about" option, a link >>> to the> GitHub repo for the code (so people can review/contribute). I >>> understand that is currently:> >>> https://github.com/expln/metamath-proof-assistant >>> <https://github.com/expln/metamath-proof-assistant> (MIT license).* >>> >>> Good point. I will add such a link. Yes, MIT license, but the new URL is >>> https://github.com/expln/metamath-lamp >>> >>> >>> *> But I think trying to answer "why can't I automate this in general" >>> is best delayed for a long time.* >>> >>> I thought on this, and finally concluded that this is not even a “nice >>> to have” but this is “must have” feature. The reasoning is as follows. >>> Users will ask me “why this doesn’t unify” or “why this cannot be proved >>> automatically”. Currently the only solution is to reproduce the case >>> locally and debug. But this is too hard because I debug by small steps and >>> I don’t see a bigger picture. Thus I conclude that I need some kind of log >>> of main events to understand faster what’s going on. So I feel like I >>> cannot delay development of this feature. >>> >>> >>> *> You could easily combine 2 & 3. Just create a first tactic called >>> "auto" or similar that tries to apply a few simple rules to automatically >>> prove a few simple/common cases.* >>> >>> I don’t have enough experience to figure out what are the common cases. >>> I need to spend some time practicing in creating proofs first. And this is >>> related to the tutorial topic (please see my response on tutorial topic >>> below). >>> >>> >>> >>> >>> >>> *> mmj2 has a few simple heuristics that it applies automatically its >>> default configuration.> You could make them either fully automatic or the >>> basis for an "auto" tactic. Code here>(I think Mario wrote more or all of >>> this):>> >>> https://github.com/digama0/mmj2/blob/master/mmj2jar/macros/transformations.js >>> >>> <https://github.com/digama0/mmj2/blob/master/mmj2jar/macros/transformations.js>* >>> >>> Thanks for the reference. I will check and return back to you and Mario >>> with questions when I will be closer to writing heuristics. >>> >>> >>> *> Even a few small automations could make a big improvement in >>> usability.* >>> >>> If anyone sees such small automations please let me know. I have >>> experience in writing code which manipulates metamath statements, but this >>> adds almost nothing to my ability to create actual proofs, so such kind of >>> small improvements are not visible to me at the moment. >>> >>> >>> >>> *> > b) highlighting syntax subtrees by clicking them> To simplify >>> replacing them, I guess?* >>> >>> Yes, but not only. This should also make easier to copy subexpressions. >>> Currently unexperienced users like me have to count parentheses which is >>> too tedious. >>> >>> >>> *> I would instead prefer an optional simple column, to the left of the >>> statement proved, showing JUSTIFICATION_NAME LIST_OF_REFERRED_STATEMENTS >>> (similar to how mmj2 works now).* >>> >>> That’s doable. I will add this to my todo list and implement in some >>> time. >>> >>> >>> >>> >>> >>> >>> *> You might want to walk through the mmj2 tutorial to see what ideas >>> are> worth stealing. I recorded it on Youtube here:> >>> https://www.youtube.com/watch?v=87mnU1ckbI0 >>> <https://www.youtube.com/watch?v=87mnU1ckbI0>> The text is here:> >>> https://github.com/digama0/mmj2/tree/master/mmj2jar/PATutorial >>> <https://github.com/digama0/mmj2/tree/master/mmj2jar/PATutorial>* >>> >>> Yeah, I watched it few times and will watch one more time with pleasure. >>> Moreover, I have now more understanding of the processes under the hood, so >>> I am able to catch more details. (When I watched it for the first time few >>> years ago it was like magic to me :) ) >>> >>> >>> >>> *> Once you're further along, I'd be happy to work with you to create a >>> tutorial> if you'd like. I'd probably want to build on the same examples >>> from the mmj2 tutorial.* >>> >>> Of course! This is a great opportunity for me to get more experience in >>> creating proofs and simultaneously help other metamath newcomers to get >>> acquainted with it. If you can provide those mmp files from >>> us.metamath.org, and additionally some json file which will work as a >>> table of content for the tutorial, then I will parse them and represent in >>> my app. Such an interactive tutorial could be a good starting point for >>> beginners. So, once you think my app is ready to become a tutorial for >>> Metamath we may start a separate email thread and discuss details of >>> implementation of such tutorial. Currently I think the tool requires more >>> testing, because I implemented some algorithms by intuition and I have not >>> analyzed everything with mathematical rigor. >>> >>> >>> *> Nevermind, I see you can already rename statements* >>> >>> In the previous versions it was not “true” renaming. Justifications were >>> not updated. But in the v6 renaming of statements updates justifications. >>> >>> >>> *> below I tell what I've come up with, in yamma.* >>> >>> Thanks, Glauco, for the ideas. I checked your test cases and I see >>> similar validations may be implemented in metamath-lamp too. >>> >>> >>> *> 'Working Var unification error: the working var &W2 should be >>> replaced with the following subformula, containing itself ( &W2 -> ph )'* >>> >>> Could you please explain why a working var cannot be replaced by a >>> subformula containing itself? It is possible in mm-lamp and I don’t see any >>> reason why it should not be possible. >>> >>> >>> >>> *> Hope this can give you some ideas.* >>> >>> Definitely! Thank you, Glauco! >>> >>> >>> >>> I implemented few new features and moved my tool to a new URL - >>> https://expln.github.io/lamp/latest/index.html >>> >>> 1) Exit edit mode on ESC, save changes on Enter on all text fields in >>> the editor. (To start a new line in a multiline text editor press >>> Shift+Enter, this is not mentioned on tooltips, but I will add it in the >>> next versions ) >>> 2) Shorter names for statements and “true” renaming of statements when >>> justifications are also updated with the new statement label. >>> 3) In substitution dialog, now it is possible to see hints why some >>> substitutions are invalid. >>> 4) A new parameter in bottom-up proofs - “Derive from root statements”. >>> It was present in v5 and it was always “true”. But it significantly >>> decreases performance and I expect it to be not necessary in many cases. So >>> I added it to the bottom-up dialog and set its default value to false. >>> Users will be able to decide if they want to use it or not. I understand >>> that I have to provide here more details on how bottom-up exactly works in >>> mm-lamp and in particular what the new parameter does. But unfortunately I >>> don’t have time right now. I will write this a bit later. >>> >>> >>> The demo video below demonstrates #3 feature and the use case when #4 >>> feature could be useful. >>> >>> >>> https://drive.google.com/file/d/1nIigII46Z8l1xk9VRWlPT9_N-VcNTh2R/view?usp=sharing >>> >>> Current latest version is https://expln.github.io/lamp/v6/index.html >>> >>> - >>> Igor >>> >>> >>> >>> On Sunday, February 12, 2023 at 9:08:43 PM UTC+1 Igor Ieskov wrote: >>> >>>> Sorry, I missed one question which could be easily answered: >>>> >>>> *> I don't see how to create hypothesis statements in the tool* >>>> >>>> This is implemented. Each statement is prefixed with an upper case >>>> letter either P (provable) or H (hypothesis). Alt-left-click allows to >>>> change it. This is demonstrated at 5:49 in this video - >>>> https://drive.google.com/file/d/1JCDffUXkb_J-TiA07aNwK9SBKyaukaA3/view >>>> >>>> - >>>> Igor >>>> >>>> On Sunday, February 12, 2023 at 1:12:24 AM UTC+1 Glauco wrote: >>>> >>>>> On 2/11/23 07:39, David A. Wheeler wrote: >>>>> >>>>> > 1) I think one of the "key" missing things is ability to help a user >>>>> > to understand why a statement doesn't unify. >>>>> >>>>> I have only an approximate idea of whether this is easy or hard, but I >>>>> will say that even modest improvements here would be helpful. For >>>>> example, it may be easier to detect particular cases than every >>>>> possible >>>>> "way" a statement can't unify. One of the more time consuming things >>>>> that happens to me when using mmj2 is that a unification which I >>>>> expected to happen doesn't, and then I need to look at (sometimes >>>>> long) >>>>> expressions to figure out what parts don't match. >>>>> >>>>> Hi Igor, >>>>> >>>>> below I tell what I've come up with, in yamma. >>>>> >>>>> First, I'll write the short story, then I'll elaborate a bit about the >>>>> theory and the challenges. >>>>> >>>>> The short story: >>>>> >>>>> yamma has two kinds of diagnostic messages for unification failure. >>>>> >>>>> >>>>> The first kind of message, suggests how to fix the unification error. >>>>> Two examples: >>>>> >>>>> "Unification error: referenced statement is '|- ph' but it was >>>>> expected to be '|- ( ps -> ph )'" >>>>> >>>>> (see >>>>> https://github.com/glacode/yamma/blob/b4864171f99f5461255e7ad8bfd2a546a9c4def3/server/src/__test__/MmpParser.test.ts#L329 >>>>> >>>>> for the full unit test) >>>>> >>>>> or >>>>> >>>>> "Unification error: statement is '|- ch' but it was expected to be '|- >>>>> ( &W1 <-> &W2 )'" >>>>> >>>>> (see >>>>> https://github.com/glacode/yamma/blob/b4864171f99f5461255e7ad8bfd2a546a9c4def3/server/src/__test__/MmpParser.test.ts#L498 >>>>> >>>>> for the full unit test) >>>>> >>>>> The first example is a diagnostic highlighted on the hyp label, >>>>> referencing a formula that doesn't match what's expected. >>>>> The second example is a diagnostic on the statement itself (the 'main' >>>>> formula cannot be unified with what's expected by the step label) >>>>> >>>>> >>>>> The second kind of messages, involves substitution of working vars. >>>>> Example: >>>>> >>>>> 'Working Var unification error: the working var &W2 should be >>>>> replaced with the following subformula, containing itself ( &W2 -> ph )' >>>>> >>>>> (see >>>>> https://github.com/glacode/yamma/blob/b4864171f99f5461255e7ad8bfd2a546a9c4def3/server/src/__test__/MmpParser.test.ts#L420 >>>>> >>>>> for the full unit test) >>>>> >>>>> >>>>> >>>>> Now, a bit of 'theory' (as far as I understand it) >>>>> >>>>> There are two categories of unification: >>>>> >>>>> 1. single statement >>>>> >>>>> 2. multiple statements >>>>> >>>>> With single statement unification, you're trying to find the mgu for >>>>> both the logical variables (the theory's variables) and the (possible) >>>>> working variables. You could use a Martelli Montanari algorithm on the >>>>> whole proof, and it will be clean and "secure", but you'll not get a >>>>> super-informative error message. >>>>> That's why, for the single statement unification, I've gone for a >>>>> 'custom' approach, that allows for some better error message. >>>>> >>>>> With multiple statement unification, you're trying to find the mgu for >>>>> all the working vars in the proof (because logical variables have already >>>>> been 'substituted'). >>>>> Here, I've gone with the 'pure' Martelli Montanari algorithm. >>>>> It can fail either >>>>> - with a 'clash fail' error (for metamath, it means two constants >>>>> don't match; something like '->' was expected, but you have '<->' ) >>>>> or >>>>> - with an 'occur check fail' (a working var should be replaced with a >>>>> formula strictly containing itself) >>>>> >>>>> Hope this can give you some ideas. >>>>> >>>>> >>>> -- 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/55b8d5f1-82f6-48a3-b032-a56725e1a5f5n%40googlegroups.com.
