> On Nov 21, 2020, at 6:22 PM, Mario Carneiro <[email protected]> wrote:
> If there is enough interest from others that I'm not the only one on the
> project, I don't mind taking the lead here. If it incorporates common code
> from mm0-rs then that will be a good excuse for me to split it off to a new
> project (the MM0 monorepo is getting pretty hefty) and maybe also expose a
> library (depending on whether this new verifier is literally mm0-rs under
> some settings or a separate executable that just links against a library with
> common code from mm0-rs).
>
> That said, I am nearing the end of my PhD and probably shouldn't be devoting
> large quantities of time to something that doesn't move my thesis forward. :P
:-). If there’s a way to combine them that’d be great.
> In that case, a good first goal would be to determine what the features of
> mmj2 *are*. Specifically, what features are actually used by people? There
> are a lot of dead relics. The main ones that come to mind are:
> * unification (kind of a requirement for any proof assistant),
> * filling in a step given all the type info (and also showing all matches in
> case some unification is possible),
> * as well as the more recent "auto step" proof search, which applies any
> theorem matching some descent criterion (and not on a blacklist).
> Anything else? There are a bunch of options in the RunParms that do stuff but
> I don't think any of them are really important (the definition checker
> excepted but that's already on the todo list). There is some documentation as
> well but it's a mixture of old stuff and new stuff and not very well
> organized. This is probably something even the less technically minded could
> help with.
Unification with past/next steps, and unification given the name of an existing
theorem/axiom, are definitely minimums, but they’re also not too challenging to
implement. Those are the keys for me. That includes, when specifying something,
immediately creating its hypotheses & supporting work variables (or something
like them for identifying “don’t know yet”).
Important item: quietly reordering rules when the proposed order cannot be
unified but another order can be. The simple automation done by leading “!” Is
really helpful. The “replace this step by that step” e.g., “d1::#1” is not used
often but is very helpful when needed.
Being able to double-click on any step & show what *could* be unified (and what
that would produce) is useful. I don’t use it as much as much you might think.
I don’t really use mmj2’s fancy search system much. That could be added later &
very simple to start.
The runParms are mostly a pain, partly because it’s a nonstandard way to do
things. Usually you just pass a filename of the file to edit. Optionally you
use options lie -? Or --long_name, and/or an init file.
> Actually, even if we branch off to a different editor mode, maybe it would be
> good to support something roughly like mmj2 for "backward compatibility" /
> getting people to use it earlier so they can speed up development.
I think that *would* be a good idea, especially if as much as possible it were
built on calls to a library. At least that would provide a familiar
alternative, and a reason to use it instead. Hopefully it would use a text
editor that can help pair parens :-).
--- 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/F4988D0C-D9EC-47E1-99A8-7E50A3EAA707%40dwheeler.com.
