>>> I think this is exactly the way the Metamath C program is working, >>> including using parentheses for performance improvement <https://github.com/metamath/metamath-exe/blob/f9a35b3155d6c1447a20f0e1717121341ff54eed/src/mmunif.c#L770> .
Thank you Thierry. It is difficult for me to understand from the code if it works the same way, but I see it also intensively uses arrays. >>> I've added an entry that links to your new tool from our list of "other tools" for Metamath Thank you David! >>> I suggest adding tooltips to every icon It is already implemented. The software I used to record the video didn’t capture tooltips. But they are present on all icons and other ui elements (like texts and text fields to show what hot keys may be used). If it is not working in your browser, could you please write what browser you use and its version? >>> Currently it uses "class1" etc. as a working variable, but these are easily confused with specific names. I suggest using mmj2's convention that &C1 is a working variable. Those are easier to distinguish, and it'd look more like mmj2 as well. Yes, I am going to implement this. >>> mmj2 does have mechanisms to prove specific patterns, but those are written in JavaScript and might be easily to copy over to a tool already written in JavaScript. My tool is actually written in ReScript (which gets compiled to JavaScript). But anyway I don’t think I could easily copy-paste the code even if the tool was written in JavaScript, because most probably we use different data structures and different algorithms. However, the idea of mechanisms to prove specific patterns is interesting to me. I had an idea to add numerous tactics to automate common proof steps, but I need to gain more experience in creating proofs to understand what common patterns exist. And if there are already some mechanisms, I would like to take a look. Could you send a link to the code in mmj2 sources, or documentation, or just write what is the core idea (whatever is easier)? >>> mmj2's ability to check definitions is awesome, but probably not critical for a proof assistant. I’ll remember that there is such area like definitions check and will return to it when I am done with the most important features. However, if you have on hand some links with description of what this is, then could you please send it as well, I will take a look. >>> I hope you'll be willing to continue work on it, it looks promising. Thank you! Best regards, Igor On Monday, January 9, 2023 at 11:34:12 PM UTC+1 David A. Wheeler wrote: > > > > On Jan 5, 2023, at 7:07 PM, Igor Ieskov <[email protected]> wrote: > > > > "it might be good to provide a README.md (and a repository with a > sensible name)" > > > > I moved the code to a new repository and provided a README file with > instructions. Please let me know if there are any issues with running the > project locally. > > > > The new repo - https://github.com/expln/metamath-proof-assistant > > Excellent! > > I've added an entry that links to your new tool from our list of "other > tools" for Metamath. The change is here: > - > https://github.com/metamath/metamath-website-seed/commit/7225664b017c800033511abdcff22f390005da34 > I linked to the redirecting web page, the repo, and the video. > > We regenerate the website daily, so that will be visible tomorrow at this > location: > https://us.metamath.org/other.html#mmtools > > I have a few quick comments about your tool: > * I suggest adding tooltips to every icon, at least with a short name. > Then people can hover over an icon & learn what it does. I would never > guess that then 5-points-star is "unify" :-). > * Currently it uses "class1" etc. as a working variable, but these are > easily confused with specific names. I suggest using mmj2's convention that > &C1 is a working variable. Those are easier to distinguish, and it'd look > more like mmj2 as well. > * Once proving in the bottom-up direction is added, for many this will > begin to be be comparable to mmj2's functionality, while being a LOT easier > to install. mmj2 has a number of specialized tricks, but I don't know if > they're as commonly used. > - mmj2 does have mechanisms to prove specific patterns, but those are > written in JavaScript and might be easily to copy over to a tool already > written in JavaScript. > - mmj2's ability to check definitions is awesome, but probably not > critical for a proof assistant. > > I hope you'll be willing to continue work on it, it looks promising. > > --- 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/5f217b0b-766c-4f6f-93dd-46e42e045e8bn%40googlegroups.com.
