Back to: mmj2
NOTE: To update the wiki your "username" must be whitelisted. Send an email to the wikilord if you are not already a user – and, if you don't care to do that, I authorize you to post as "ocat" for the purposes of mmj2 feedback and problem reports, etc. (Just put some initials on your edits so I know who is doing what…)
ALSO, you may get the "Cannot acquire main lock" error message when attempting to post to the wiki. In this case, hit the Back button on your browser, open a new window and go to RecentChanges then click on Administration, then Unlock Wiki. Wait, and then return to your original post and click on "submit" again.
Previous Version of Feedback: mmj2ProofAssistantFeedback20080217
(Complaints about other aspects of mmj2 – general grievances -- should go here: mmj2Feedback )
Complaint Number 1: 17-Feb-2008 – ocat
Complaint Number 2: 19-Feb-2008 --ocat
Complaint Number 6: 27-Feb-2008 --ocat
File/New Proof or File/New Next Proof create a "skeleton" proof with the 'qed' step as follows:
qed:: |- blah blah blah
This is "ok", but really it would be better to output the 'qed' step as:
qed:?: |- blah blah blah
This is better because a) an hypothesis is nearly always going to be necessary, unless the new theorem is simply an instance of a previous theorem, which is uncommon at most; and b) with "?" in the Hyp field, the new Step Selector Search can be used immediately just by double-clicking the 'qed' step – instead of requiring the user to enter something in the 'qed' Hyp field just to get some results.
By the way, the new Step Selector Search feature is almost identical to the enhancement that Norm requested at least twice. He wanted a "hint" type of feature where the program would show, for a step, only the possible unifying assertions for that step – in other words, there would be no "invalid" inputs, which is the way the Metamath Solitaire program works. Unfortunately, I couldn't get my head wrapped around Norm's request until the Work Variables enhancement was written, along with the new "StepUnifier" for unifications involving work variables. Also, I needed fls request implemented for having the mmj2 program be aware of the input cursor's location. In the end, my code converged to what Norm was asking for (with a couple of generalizing tweaks.) So, I really can't take credit for any of the inventions in the newest version of mmj2!
The good news is that my iMac Mini, circa 2007/$599, which runs 1.6GHz Intel Core Duo (2 processors) with 512MB RAM completes Proof Assistant startup in about 9 seconds vs. about 16 seconds on my HP desktop, circa 2001/$1100, which runs a 1.8 GHz Intel Celeron with 256 MB RAM (DDR SDRAM).
It is difficult to say how much of the 50% (approx) speed-up is attributable to the Java Runtime Environment's extensive built-in use of multi-threading, which, one hopes is distributing the load automatically across both processors. It may be that the OSX operating system and the iMac in general have less overhead than the XP system. And, that the iMac has more memory and overall uses more advanced hardware, is no doubt a positive. Anyway…this is interesting and good news. I would be interested in hearing about your experiences on a modern XP or Vista machine running on Intel Core Duo.
In the problems category:
Complaint Number 3: 25-Feb-2008 --ocat
Complaint Number 4: 25-Feb-2008 --ocat
Complaint Number 5: 25-Feb-2008 --ocat
Complaint Number 7: 3-Mar-2008 --ocat
Complaint Number 8: 3-Mar-2008 --ocat
Complaint Number 9: 3-Mar-2008 --ocat
In the "Not a problem" category, the issue I had with the ProofAsstFolder RunParm turns out to be my bad… Assume logon as user "Me", with mmj2jar stored in directory "A". Then in Utilities program Terminal, the startup directory is "Me". (And using "pushd A/mmj2jar" takes you into the mmj2jar directory.) The RunParms.txt ProofAsstFolder option just needs to be updated (manually) like this:
So the whole problem was me not understanding what I was doing on the iMac… and I still haven't learned how to write a script to startup mmj2, and I am starting up the mmj2 by copying the execution line from mmj2.bat and pasting it into the terminal window, and pressing return:
java -Xincgc -Xms64M -Xmx128M -jar mmj2.jar RunParms.txt
So, mmj2 basically works but needs some fine tuning on the iMac running OSX.
Here is a fairly elegant (proposed) enhancement with user-controlled ambitions: a re-entrant proof step "sub-proof" prover available via right-mouse click or menu key (designated step at the input cursor location), with parameters controllable by the user: 1) max search depth; 2) breadth or depth first search. The re-entrant sub-proof prover would use the given proof step's hypotheses as the hypotheses for the sub-proof, with the restriction that neither the given proof step or its hypotheses can be "in error". If successful, the sub-proof's derivation would be inserted into the current proof. This enhancement is difficult and ambitious but it would, at least, be worthy of the attempt (and it can be coded with all new code or be tightly integrated into existing logic.)
The key idea here is to restrict the prover search tree to something that is manageable and user-controlled. By restricting the hypotheses which may be considered for a proof step to those specified on the proof step, the number of combinations which must be examined is reduced, and furthermore, the work of figuring out which previous proof steps are irrelevant to the current step is put in the user's hands.
So consider how this would work for proof step "99"
h1:: |- blah blah 90:?: |- blah blah 99:1,90: |- blah blah
The user specified "1,90" for step 99 and then right-mouse clicks proof step 99 and selects "prove" (or uses a menu option while leaving the input cursor on step 99). If the prover finds a proof of step 99 using either 1 or 90, or both or neither, the derivation is inserted into the current proof and step 99 is automatically updated with the Ref and actual hypotheses used. If no proof is found, the user can retry the operation with a deeper search depth, and perhaps switch from breadth-first searching to depth-first.
Sounds great, huh? No?
Well… This feature can be used for the 'qed' step of a proof. That is, to generate an entire proof. But that will really only be helpful for simple proofs, especially those at the start of a Metamath database (e.g. set.mm or ql.mm) – as the number of theorems to be searched grows, and as the number of proof steps increases (max depth), the algorithm will bog down in the combinatorial explosion of possibilities. However, for individual proof steps guided by a knowledgeable user the reentrant subproof generator will be very helpful and will reduce the amount of work – as well as minimizing rote memorization of theorems, letting the user focus on the math instead of the label names in the Metamath database.
Here are the parameters which I foresee as possibly being useful to users:
As I consider this programming task, I see that there is a "short-cut" which employs the existing unification algorithm in mmj2, mmj.pa.StepUnifier.java. However, this would restrict the search to a single search execution path – no concurrent searches for alternative proofs. Given the fact that multi-core computers with shared memory access are now the norm, a concurrent approach would be far better even if it means additional coding work (better to write code just once.)
I also foresee:
Any feedback, questions or constructive criticism? I think this is the only enhancement worth doing – at least it seems worth doing even if, as usual, I don't get paid :-) Perhaps that is the essence of "open source", that you do what you do because you gotta do what you gotta do…
OK, I am "officially" beginning this project, which I will call "Step Prover" (highly imaginative :0-)
I expect it to be ready for your use within six months, at the latest, and my hope/goal target date is 1-Feb-2009 but I cannot know for sure until I devise the search algorithm and the new unification algorithm – as well as the multi-threading control mechanism :-)
My first task is to write an incredibly long document which will likely never be read, but will, I think, help me to avoid design and coding errors.