HomePage RecentChanges

mmj2ProofAssistantFeedbackV20070716

Previous Version of Feedback: mmj2ProofAssistantFeedbackV20061101

Feedback About the new mmj2 Proof Assistant GUI

The policy here at MMJ2 Research Labs, LTD. is to listen to our customers' complaints. We care deeply about your feelings, thoughts and suggestions. Be sincere and honest – but please substitute combinations of "!", "@", "#" and "$" for swear and cuss words…

Complaints about other aspects of mmj2 – general grievances -- should go here: mmj2Feedback

NOTE: It is not necessary to be a member or to register, log-on, or otherwise prepare for making a comment. Simply enable "cookies" on your browser, click on "Edit this page", and type in your comment/question/note. Then "save". It is desired that you identify yourself in some way, and perhaps even add your name to the "guest" list. Make up a pseudonym if you are inclined and use that, if your are security conscious. --ocat


Links


Things I like about it

Thanks for adding the $d statement generating feature. I've always used and liked mmj2 (every proof I've submitted to set.mm was done with mmj2) except for the annoyance of having to add $d statements. Now proof finding is quicker, easier, and less tedious. :) --steverod 19-May-2007

Thanks. I appreciate the info (I had assumed you were using it to accomplish the many feats I have observed at metamath.org :-) --ocat

Installation Grievances

Suggestions and Things I do not like about it

1. The proof text area is always in "Insert Mode", and the insert key doesn't toggle between replace and insert.

2. It does not output proofs in Metamath compressed format.

    --> This is not impossible, but it is computationally
        intensive. Given that Metamath.exe now has an
        import/export facility for mmj2 Proof Worksheets,
        the priority of this item is lower than low. The
        reason why it might be done is that there are 
        interesting algorithms for checking for repeated
        subproofs and this is an active area of research.
        My idea is to create a hash key for each node of
        a proof tree and then check a hash table to see
        if the sub-proof already exists for the proof. 
     

3. A new design of the PA screen would be easier and better. It should use a "tree" metaphor where the user works on just one proof step branch at a time, and the program only unifies one step at a time.

    --> This would simplify certain aspects of the coding,
        particularly those written defensively against 1000
        step proofs requiring unification. It would free
        things up and allow the screen and CPU resources to
        be brought to bear with focused intensity on the 
        problem of proving a single step! 

4. It would be nice to see the 'qed' step (assertion) on the first display page when browsing existing proofs.

    --> This behavior could be added as a RunParm option, and
        possibly via a menu option. Not hard. 
     

5. The 'Unify+Get Hints' hint messages should be expanded to show the formulas of the hint assertions, instead of just the labels.

   --> OK. Can that be one long text line per assertion, with
       text wrapping (e.g. ax-mp: ph && ph -> ps ==> ps) or do
       you care about the full TMFF rendering of these messages
       (I assume not...as that would consume vastly more space.)
       In theory, a future version of PA could test each hint
       and see which is a "best fit", and automatically insert
       that with any needed hypotheses -- you could then Edit/Undo
       if dissatisfied (no idea how to guesstimate a "best fit"
       though, and also, shouldn't the user do some of the work?)
     

6. The 'Derive' feature ought to conform as closely as possible to the way the metamath.exe Proof Assistant works with respect to entering the Ref labels in RPN order – while requiring minimal (or no) other input. As is, for one thing, the mmj2 PA Derive inserts a 'dummy' variable into a generated hypothesis as replacement for a variable in the Ref'd assertion which is not substituted-for in the (partial) unification substitution tree. In theory mmj2 could pick an unused variable from the Mandatory+Optional Frames – or, 'dummy' variables could be enhanced and made 'real' names of substitution expressions (expanding the spec of a Proof Worksheet). Further analysis on the differences between and reconciliation of Metamath.exe and the mmj2 PA's is needed.


7.

Hi O`Cat and Raph.

On connectivity since I often use Mmj2 I will use it to show how different formats can lead to difficulties. When you are working on a proof you simply use eimmexp.cmd and eimmimp.cmd to transfer it from Mmj2 to Metamath and back. It is a bit long but it's not really important. The very problem is that the Proof Worksheet format and the mm format doesn't fit together. Suppose for instance that I have begun my proof in Mmj2. I have a d statement, some comments and different scraps of proof that are not connected together. If I want to export this proof to Metamath I must remove the d statements and the comments otherwise eimmimp.cmd doesn't work. Once I am in Metamath the non connected scraps will be linked by dummylinks. Then I work on this proof in Metamath and I translate it back to mmj2. It means that now the proof has no d statement and no comments any longer and that the non-connected statements are now connected with dummy links. Not exactly the same proof as you can guess. The consequence is simple I don't use d statements, nor comments, nor unconnected scraps of proof because I know that I won't be able to export my proof. And to export my proof I need ! On the other hand d statements, comments and unconnected scraps of proof are in my opinion very important features of Mmj2. I wonder if there is not a way to allow to use these features and to ensure that Mmj2 and Metamath are completely connectable. Suppose that a window in Mmj2 contains the main proof. In this window there is no d statement, no comment and there is only one scrap of proof. This way Mmj2 and Metamath are perfectly connectable. In other windows I have added some comments, a d statement and I've tested other unconnected scraps of code. Since they are not in the way of the main proof they can't alter the connection between Metamath and Mmj2. And since we use the extra features of Mmj2 it means O'Cat's intent is respected. – fl 30-Dec-2006

Hi fl - you raise interesting points concerning communication of unstructured data (Je regrette les horreurs que vous éprouvez.) It is not so easy to retrofit metamath.exe to use Proof Worksheets, and eimm.exe is like a "patch". To the main point, can you go to the mmj2 Proof Assistant wiki page and explain why you need to go back and forth between mmj2 and metamath more than once during proof invention? Perhaps mmj2 can be enhanced to eliminate these multiple round trips! And perhaps – horreurs – mmj2 can be modified to generate the necessary $d's for you. The problem of comments is fixable, perhas, since the Metamath .mm format allows comments between any tokens, and in theory eimm.exe could export embedded proof comments to a Proof Worksheet. The problem with dummylinks in Metamath is probably unfixable due to the basic design of the Metamath Proof Assistant, which is perhaps inflexible. Essentially then, I am saying, tell me how to make mmj2 fit your needs so that it is unnecessary to export prior to the final update of the .mm file (this would not preclude using metamath.exe simultaneously for searches, etc.) --ocat 30-Dec-2006

Hi O'Cat, hi Raph and happy new year,

I will go to the Proof Assistant wiki page to explain you why I specially need to go back and forth between metamath and mmj2 but I'd like to insist on the general idea of easy communication between softwares before. I will give an example. My favourite text editor is emacs. But many years ago I would use vi. In fact we could think I've completely abandonned vi. But it's wrong. I still use vi for many reasons. I use it less than emacs but I use it. In fact these softwares have been designed with very different interfaces. And I can't really say that one is better than the other. Depends on the occasion in fact. So as you can imagine I would be very annoyed if the same file format were not used by emacs and vi. It's true for other softwares as well. For instance midnight commander is quite an old piece of software. However I often come back to it. (By the way if somebody can send me an exemplary of the venerable Turbo debugger I will be very happy.) fl 2-Jan-2007

Hi fl, happy new year.

I am sorry that your experience with mmj2 <<==>> eimm <<==>> metamath is lossy. Originally eimm.exe did not exist :) Then Norm spent a few moments and typed it in. In theory he can make changes, assuming that the effort can be cost-justified and it pleases him to spend his time that way. He never set out to fully translate mmj2 ProofWorksheets?, especially not incomplete or error-ridden proofs-in-progress – that is hard work and intricate! Plus, the Metamath Proof Assistant doesn't even do Distinct Variable Restrictions. I think it would be relatively simple to delete the "dummy proof" steps and re-convert back to just "?" (missing / unknown hypotheses). He might even be able to cache the original Proof Worksheet Header, Footer, $d's, and Comments – and then re-insert the modified proof; that might not be crazy-hard.

I share your concerns about communication between software packages that ought to be able to interoperate well. I am now investigating OMDoc, and I think it may interest you as well. Of course, assuming that "mmj3" wrote to OMDoc standards, there is a strong likelihood that mmj2 would stay ignorant about some of the information in an OMDoc object.

For now I am happy to see that you are contributing hundreds of theorems to Metamath, and I assume that you continue to use mmj2, remaining 95% happy with its performance.

P.S. fl The original "design" of the mmj2 Proof Assistant intended for the user to manually copy a finished RPN-format proof into the .mm file used. Then eimm.exe allowed less painful importation/export, but lossy. So what, I ask, do you need from the metamath.exe that mmj2 does not provide in Proof Assistancy – besides searching with wild cards, which you could do even without eimm.exe by simply running mmj2 and metamath simultaneously. I cannot guarantee a fix for what you want, not within the existing PA framework, :-0)

--ocat 2-Jan-2007


I am tied up with some things right now that are slowing down even set.mm, and I won't have time to work on eimm for a little while. But I tried to make the comments in eimm.c reasonably clear, if someone wants to enhance it to make it work in a way they are happier with. It is not terribly difficult code, mostly just parsing the worksheet and the MM-PA output, with lots of bug checking (especially that the expected command sequence was used to generate the MM-PA output). The eimm.c program is about 900 lines long, excluding a standard string library taken from metamath, and the import and export functions are each around 300 lines each. Some observations:

1. Retaining comments is a difficult problem. Although the Metamath syntax allows them in proofs, as a practical matter it is difficult to keep them associated with proof steps when proofs are compressed, minimized, reworked, etc. So, they are just discarded by any of the save proof and save new_proof commands in the metamath program, and I don't see that behavior changing anytime soon if ever. The question is, can they be retained in the worksheets?

I suppose that if a previous worksheet exists during export, the program could attempt to put the comments back into the new worksheet - but correlating them with the proof steps after the proof has undergone a number of transformations doesn't seem easy. Perhaps you can think of an approximate matching algorithm that works most of the time for minor changes; if so, feel free to put it in the program. Perhaps it could flag comments (with a special notation in the comment itself - not with error messages during the program run, which would be more difficult to match up if anyone even pays attention to them flying off the screen) that it couldn't figure out where to put them, and just make a best guess by putting them somewhere between the surrounding ones that it could figure out.

Note, by the way, that a previous version of a file created by eimm.c is not immediately deleted but is renamed to filename~1, any previous filename~1 renamed to filename~2, up to filename~9; a previous ~9 is deleted. Using this philosophy in metamath has saved me a lot of grief over the years due to stupid editing mistakes, even though it clutters up the disk - so every now and then I do rm *~[1-9] or rm *~[2-9]. Or you can add that to the eimm script if you hate them.

Confession: during the input .mm file parse – low level routine – mmj2 discards comments that are between tokens in a Metamath statement. When I wrote that code I overlooked the Metamath.pdf specification allowing them, and I had to write a crufty patch to make them disappear within the low-level code (didn't want to re-formulate the algorithm.) Also, not until I wrote the mmj2 PA did I fully understand the deep structure of a Metamath proof; considering it as an array of statement labels in RPN sequence, I could not imagine a good way to associate a comment with an individual "step". Now I see that the major steps correspond to (end at) the assertion labels for non-syntax axioms and theorems/derivations. So a proof might have 10 major steps and contain 296 minor steps. But even that is inadequate because of repeated sub-proofs: the final major proof step's proof tree contains as sub-trees the proof trees of the previous major proof steps.

2. I think that the dummylinks that are inserted by import (in order to create a legal MM-PA partial proof) could probably be stripped back out during export without a whole lot of difficulty, thus restoring the orphaned status to isolated proof scraps, although I haven't looked at it.

I think you know that dummylinks in a finished proof are automatically cleaned out by the MM-PA "minimize_with */brief" command, with any unused proof scraps they connect to discarded.

3. I am unclear on what the issue is with $d's. They are not handled by MM-PA, and even though this is an item on my to-do list, I won't get to it soon. Elsewhere on this wiki I've wondered if I even want them handled in MM-PA, because they may just be a nuisance during proof development, and it may be easier just to fix all at once in the end anyway like we do now. As for automatic generation of them, that would be a nice feature for metamath and/or mmj2; I'll add it to my to-do list for metamath. But for now, there is a script I use to collect them on the metamathMathQuestions page. It isn't completely automated, but the time I spend putting them in at the end is a very minor part of the total time I spend on the proof itself.

We have already established that two theorems that are identical except for their $d stipulations are truly different theorems. And a little-advertised aspect of the mmj2 PA is that the unification search process will attempt to hunt down the correct unifying assertion – the one without any $d errors. That took a fair amount of coding work, but it is done now. Also, if the user inputs a label and $d errors result, the program reports back on any alternate unifications.
Yes, metamath's MM-PA definitely assumes you know what you're doing and requires experience to use it effectively. It lets you construct proofs that won't verify when you add in the desired $d's. It lets you construct partial proofs with unifications that are impossible when you try to fill in the syntax-building steps. It is only when the proof is done that you can know for certain that it was done right. norm
I think that automatically generating $d's in mmj2 would be very doable. Also, the Proof Worksheet format includes a "$d" statement which, in theory, could be imported/exported by eimm. The $d stipulations of the Proof Worksheet are additive to the existing $d's in the theorem under discussion and normally appear at the beginning of the Proof Worksheet just after the "Header" statement.
.
With respect to eimm handing incomplete and/or error-ridden Proof Worksheets, I am skeptical because the amount of work in parsing and validating a Proof Worksheet is considerable. What I want to know is what motivates the user to make multiple round-trips between mmj2 and metamath so that the omissions and inadequate functions of mmj2 can be remedied. --ocat

norm 4 Jan 2007


norm here again: While I know it takes roughly 10 times as long to read someone else's code as to rewrite it from scratch, :) you may want to give at least a passing glance at the algorithm in the Metamath Solitaire applet's "Proof Assistant". It may contain some ideas you can utilize for the mmj2/3, particularly since it has complete and foolproof $d handling. Compared to metamath's MM-PA, it is an extreme in the other direction.

The algorithm is simple, clean, and robust, I think. Its main requirement is that it needs to work with Polish notation, but mmj2 already parses things to a form I assume could be converted to Polish, if it doesn't already use Polish internally. I haven't analyzed its speed but am unaware of anything about it that is fundamentally slower than other unification algorithms. The limitations of MM Solitaire are not with its algorithm, but with the program wrapped around it, which is just a simple-minded applet demo of the algorithm. What the algorithm needs is a proper program to contain it. – norm 4 Jan 2007

That is a great idea. It is also in line with one of fl's suggestions about focusing on one step at a time in the PA (which would allow all resources to be brought to bear in one place, for one purpose, for the benefit of the user).
And for your benefit as well I think since sometimes mmj2 enters loops for reasons totally obscure to me. But I don't know what you mean by tree. If it means that you want to change the interface please, my dear O'Cat, don't ! The plain text list design pattern that you use currently is perfect in my opinion. The only interface change I would appreciate is a multi-tab interface. – fl 5-Jan-2006
"tree" is internal – the data structure (can be converted to Metamath RPN format). The "plain text list" won't change, but maybe an "mmj3" will happen some time :) I don't know about multi-tabbing mmj2's PA either – it might be cheaper to just buy you a second computer :-)
I think multi-tabbing would be a great feature for mmj2 or mmj3. An example of very good editor using that technic is kdevelop : [[1]]. PA means what ?
If you see a "loop" it would probably be a thread exception halting activity: hit the Cancel menu item to get cursor control back, then switch back to the Command Prompt window and you should see a mini-dump from the Java Runtime Environment. Then please copy the info and shoot it to me. --ocat
I will but you should try to make long proofs with mmj2 otherwise there will be many phenomenons that you will never be aware of and I think if you don't force yourself to do that you will never be able to take the good design decisions. In fact a directory of test cases is not enough. Free weight is mandatory in computer design as in body building– fl

Re: "While I know it takes roughly 10 times as long to read someone else's code as to rewrite it from scratch, :)" ==> So, you do have a sense of humor! Haha. I don't fear your code :)

--ocat

Bugs

5-Jan-2007: "…sometimes mmj2 enters loops for reasons totally obscure to me." --fl

==> If you see what appears to be a "loop" it is probably a thread exception that has already halted activity. Hit the Cancel menu item to get cursor control back, then switch back to the Command Prompt window and you should see a mini-dump from the Java Runtime Environment. Then please copy the info and shoot it to me along with a copy of the Proof Worksheet at the time of the "incident" (you can Edit/Copy from the GUI text area to capture the proof text as-is).

A "Thread Exception" could be caused by a Null Pointer Exception. Another possibility for an apparent "loop" is an Out Of Memory or Heap shortage (I saw this, I think, when texting Sphinx-4). To check memory click on Help/About, which does a garbage collection pass and then reports on memory utilization – if your machine is running low on memory (I don't know how much you have), there are RunParms to reduce utilization when the .mm file is loaded. Look in mmj2\data\runparms\windows\AnnotatedRunParms?.txt at:

        LoadEndpointStmtLabel,FermatsNextToLastTheorem    
        LoadComments,yes     
        LoadProofs,yes     
     

Switch to "LoadComments?,no" and "LoadProofs?,no" for a big saving, and if your theorem of interest is not near the end of the file, specify "LoadEndpointStmtLabel?,loc-after-label" where loc-after-label is the label of the .mm statement prior to the insert point of your theorem.

If possible, send me the diagnostic info ASAP so that I can get your code fixed up. You are my best customer and I want you to be happy :) --ocat 5-Jan-2007

Thank you I will try use mmj2 intensively to get some nice "loops".

Hi, I didn't mention this earlier today but the new release has suggested options for the Java environment as a workaround to various memory related "issues". I described them here: mmj2UsageNote20061019. If you are using the pre-11/1 mmj2.bat then that might be a contributing factor to what you perceive as a "loop". The mmj2.bat should look basically like this:

java -Xincgc -Xms64M -Xmx128M -jar mmj2.jar RunParms?.txt

Those options are described in the link (and the mmj2.zip). I would prefer to find out that there is a memory leak in the JRE than a null pointer in mmj2 :-) If, as you say you are doing these huge proofs then "incremental garbage collection" and large initial memory allocations would help – and the memory-conserving RunParm? options I described above. Also, downloading the latest JRE version from Sun would be a wise idea (I know for a fact they patch Java a lot – it is not at all bug free!)

--ocat 5-Jan-2007

Talk