> 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/0F0468AD-B017-4E6D-AC72-8ED81DC99A88%40dwheeler.com.
