Back to: mmj2

note about the wiki

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.

other links

Previous Version of Feedback: mmj2ProofAssistantFeedback20080217

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

Feedback About the mmj2 Proof Assistant GUI

Windows

Complaint Number 1: 17-Feb-2008 – ocat

• Request for TMFF Reformat triggers Save with Yes/No/Cancel dialog box. I do not think a reformat should trigger a Save dialog. (Originally it seemed more drastic but now that the Edit/Undo (Ctrl-Z) is available a simple reformat is not a big deal.)
• When a TMFF Reformat request is made and the proof is new, and changes have been made, the whole File Name dialog is invoked, and after going through the humongous hassle of saving the file…it seems like the reformat isn't done! Dagnabbit. (This is a low-level bug with the obvious workaround of just saving and then doing another reformat. So no quick Patch .jar upload just for this thing.)

Complaint Number 2: 19-Feb-2008 --ocat

• Extra – empty – selection lines at the end of the results in the Step Selector Dialog would allow the list to be scrolled down so that the bottom selection line could be displayed at the very top of the dialog. This would be helpful because it is handy to be able to move the dialog down so that the Proof Worksheet can be viewed simultaneously.

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!

Mac Issues (Apple J2SE 5.0 Release 4)

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.

Whatever…

In the problems category:

Complaint Number 3: 25-Feb-2008 --ocat

• The "alt" key is the iMac "option" key, and this is ineffectual for the Edit Menu on the Proof Assistant. I surmise that the Terminal utility has co-opted the Option key for its own purposes.
• It may be that this is fixed in J2SE 5.0 Releases 5.

Complaint Number 4: 25-Feb-2008 --ocat

• Setting the Proof Text Columns and formula length maximum to 100 (from 80) via the startup RunParms? without changing the default font size of 14, produces a different result on the iMac: the Proof Text Area window is output as just two lines long! This is, I think, because the line length is bigger than the Frame size with the given font size. In order to make this work, the font size needs to be decreased to 12 when the number of columns is increased. With bigger LCD screens these days it is reasonable to use 100 column displays. (I alse turn off "bold" to make it look better. You may wish to change the TMFF Format Number in the start-up RunParms?. I'm liking 10 these days.)

Complaint Number 5: 25-Feb-2008 --ocat

• Ctrl-8 invokes the Step Selector Search but also inserts an "8" in the Proof Text! That is wrong and definitely incompatible with the Sun Java 1.5. The "workaround" to this, and I guess Ctrl-9, is to not use Ctrl-8 or Ctrl-9. Double-click instead of Ctrl-8ing and use the Unify/Reshow Step Selector Dialog menu item (or just move the dialog off to the side manually instead of "hiding" it.)
• It may be that this is fixed in J2SE 5.0 Releases 5.

Complaint Number 7: 3-Mar-2008 --ocat

• Message text not line wrapped on call to Yes/No/Cancel Dialog Box – another Apple incompatibility, though perhaps fixed by more up-to-date version of Java on OS-X.

Complaint Number 8: 3-Mar-2008 --ocat

• File types allowed in File/Save As dialog not displayed properly (another incompatibility between Apple and Sun.

Complaint Number 9: 3-Mar-2008 --ocat

• There appear to be a lot of differences between the Sun and Apple implementations of the Java "Swing" classes (Swing is the GUI framework layered on top of their original AWT GUI classes.) So far the "bugs" in the Sun version have been mere annoyances and do not prevent the mmj2 Proof Assistant GUI from functioning. HOWEVER… assuming that the mmj2 software can be released for use with OS-X without running the parallel/regression tests is unwarranted. Next release run the parallel/ regression tests on the iMac and perform file compares to ensure that the full suite of mmj2 tests performs flawlessly on OS-X – until that is done people should be advised to use mmj2 using Sun's Java and to regard other implementations of Java as experimental with respect to mmj2.

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:

    ProofAsstFolder,A/mmj2jar/myproofs
    

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.

--ocat 27-Feb-2008