Previous Version of Feedback: mmj2ProofAssistantFeedbackV20061101
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
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
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.
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.
– 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
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
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
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