On 6/6/25 22:42, Marlo Bruder wrote:
Hello there metamath community!
I wanted to ask you all 3 questions related to proof assistants:
1. What proof assistant are you currently using?
mmj2
1. What are some (not so obvious) features of your proof assistant
that you like and that you would like to see recreated in future
proof assistants?
The screen is mostly devoted to my proof, with a minimal space taken up
by navigation widgets and the like.
I can copy-paste .mmp files between set.mm and iset.mm and, insofar as
the theorems being referenced are present in both, it works.
This one is kinda dumb but I'll state it anyway: the format of the
generated proof differs visually (in line length) from the output of a
minimized proof from the metamath-exe minimizer, which I use to notice
whether I forgot to run the minimizer.
I use comments (lines starting with "*") extensively (to make notes to
myself, comment out proof lines, etc).
1. What are some things you don't like about your proof assistant
that future proof assistants should avoid?
Ideally the proof assistant would be a bit better able to fill in
certain things like substitutions (in fact, under some circumstances I
think older versions of mmj2 were better than the one I am using now).
mmj2 has a lot of rough edges (menu items that don't work, keystrokes
which can destroy your proof unless it was saved, etc). Perhaps it goes
without saying that I'd prefer not to have such things but maybe the
larger lesson is to focus on fixing annoyances as much as implementing
more features.
Lastly I still had a few more questions about metamath and set.mm:
* What does the ! at the beginning of statements do in mmj2? I think
I read somewhere that it was an undocumented change. Is anyone
nevertheless able to come up with an informal description of how
it impacts the unifier?
It tells mmj2 to try to find a proof for this step. Without the "!" mmj2
will mostly leave the line alone, without proving it in terms of
previous steps. I use this for example when there are steps in the proof
which I know I can't prove, but which I'm not ready to comment out yet
(and thus I don't want the line without ! to pick them up).
* I want to be able to syntax highlight variables without having to
hardcode the colors. Right now it seems the only way I can do this
would be to parse the htmlvarcolor setting, which would be pretty
tedious. Would it be possible to add a varcolorcode setting to the
typesetting comment, which assigns a variable colorcode to a
typecode? And if not: How does mmj2 derive the colors for it's
syntax highlighting? Are they hardcoded?
Don't know about mmj2 but strikes me as sensible to add something like
varcolorcode.
* In mmt1 the table of contents is replaced by an explorer on the
left side of the screen, similar to e.g. vscode's file explorer,
only with headers instead of folders. This however requires that
all headers are exactly one header depth below their parent
header. set.mm follows this rule in with all headers but 3 in Jim
Kingdom's mathbox. Would it be ok (specifically for Jim Kingdom
himself) to change the header depth of those 3 headers?
Ideally we'd have a tool to enforce this which we can run on pull
requests, but seems like a good idea. If I get around it I'll fix it but
if you want to make a pull request to my mathbox that's fine too.
--
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 visit
https://groups.google.com/d/msgid/metamath/6b368bee-a7e4-47c0-aba6-f70765de2d92%40panix.com.
