> On Jan 10, 2023, at 4:06 PM, Igor Ieskov <[email protected]> wrote:
>
> >>> 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?
I see, it *does* work, but I had to wait longer than expected before they
appeared. Perhaps I'm just too impatient :-).
> >>> 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)?
The main mmj2 repo is:
https://github.com/digama0/mmj2
mmj2's algorithms aren't sophisticated. Here's a key file for its automation
capability:
https://github.com/digama0/mmj2/blob/master/mmj2jar/macros/transformations.js
> >>> 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.
The definitions check algorithm is probably best understood by viewing the
"conventions" page section "Additional rules for definitions". Go here:
https://us.metamath.org/mpeuni/conventions.html
The metamath language itself doesn't distinguish between axioms and
definitions, but
in practice we *do* maintain such a distinction as explained there.
The mmj2 code for the definition check is here:
https://github.com/digama0/mmj2/blob/master/mmj2jar/macros/definitionCheck.js
By the way, there's a trick you could use in your JavaScript proof assistant:
encode the current proof-in-development in the hashcode ('"#" and text after
the URL).
Every time there's an edit, update the hashcode. That will give you undo/redo
for free, make it trivial to save/load proofs, and it would also make it trivial
for people to share proofs with others (just share a URL).
I recommend you not store the entire program state (the .mm files would be
enormous),
though the names of the databases might be helpful. See:
https://www.scottantipa.com/store-app-state-in-urls
https://news.ycombinator.com/item?id=34312546
I'm sure there are pros and cons, but I thought I should mention it.
--- 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/A6951314-469D-42E2-9536-D457207C456F%40dwheeler.com.
