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. >
Here is a short list of things that I heavily use in mmj2 (I'll throw more if they come to mind): - the General Search page: I really use it a lot (as I wrote, I use a Mel O'Cat version where the Search has been fixed/enhanced) - ctrl+G > Theorem label (loads from the System Area a proven theorem and "translates" it in .mmp format; it can be either be fetched from the .mm loaded file or from a .mmt file in the working folder) - right click > Reformat Step: Swap Alt (takes a single line and shows it on multiple lines, with "nice" indentation; I wish there were a key shortcut for this one) - ctrl+O (Reformat Step applied to all the lines in the current .mmp file) - ctrl+R (when every statement is on a single line, ctrl+r indents them nicely, so that you can see immediately orphan steps) - Edit > Set Soft DJ Vars Error Handling > options 3 and 2 (option 3 is my "normal" mode, but I use option 2 a lot, when I want to remove dv constraints) - ProofAsstIncompleteStepCursor,First (this made my productivity boost n times... :-) ; after a ctrl+u it places the cursor to the first unproven line ; I can type dozens of ctrl+u without having to leave the keyboard) In the first phase I'll be happy to use the new tool and go back to mmj2 when some feature is still missing. Please, let me know what's the best environment to set up to contribute to the new tool: - VSCode + RUST seems to be the candidate, right? (if it were possible to have a portable environment it would be a plus) - at least Windows + Linux is a must, I guess Glauco -- 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/a0396e3b-8249-4d19-95c5-d33fd6af02ebn%40googlegroups.com.
