HomePage RecentChanges

mmj2FeedbackV20070716

Back to: mmj2

Previous version of mmj2Feedback: mmj2FeedbackV20061101

Questions/Comments About mmj2?

Dedicated page for feedback about the mmj2 Proof Assistant GUI: mmj2ProofAssistantFeedback

Feel free to use this page for other items…

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


Of great significance to current and potential mmj2 users, it appears that Sun Microsystems is this close to GPL'ing Java (SE and ME) – Sun Set To Move On GPL License For Open-Source Java

That is a big win for mmj2. Nice! Java is a good language for this sort of project. I like the garbage collection, no pointers (per se), and array bounds checking. I don't like "Swing" and certainly plan to hunt for an alternative if, perhaps, I do attempt an ambitious GUI scheme involving lots of graphic rendering and novel input methods :)

--ocat 12-Nov-2006

Perhaps now someone will figure out how to speed up the Java start-up time. On my 2GHz laptop the Metamath Solitaire applet, with 3000 lines of code, takes over 15 seconds to start up. This is compared to say the Metamath program, which has 30,000 lines of code but starts up in 6 msec on my 466MHz Linux machine, i.e. 25000 times faster in terms of (the admittedly meaningless measure of) start-up time per line of code, even disregarding CPU speed. I have no idea what the issues are, but perhaps if it were modularized so that only the components needed to run the program were loaded, and nothing else, it could be speeded up a 100 or 1000 times for small programs. Now that it's open sourced, maybe someone will be inspired to look into what can be done. – norm

Traces

May I suggest O'cat that it is very difficult to find the important information in the traces of mmj2 (either when the software starts or when we "compile" a proof). In the film by Forman (?) it was reproached to Mozart that there were too many notes. I'd like to say "too many words", my dear O'cat, "too many words". – fl 1-Dec-2006

You remind me of my brother Mal :)

I should really provide French output messages seeing as France is home to one-third of mmj2's customers.

In my opinion, concerning the number of words it would be worse: we, French, need such a large amount of words to succeed in saying something! Try Turkish. Turks are very concise. Normal, they are farmers, the sort of people who only pronounce two words in a day. – fl 2-Dec-2006

I have pictures to show precisely what I mean but I don't know how to upload them. Any idea ? – fl 3-Dec-2006

Yes. For Windows…

The Command Window has Sysout and Syserr printstreams – text. So, either pipe the output to a file:

     mmj2.bat > sample.txt
     

Or, click on icon in upper-left corner of screen, then select Edit, then Mark. Then select text using mouse or cursor and hit Enter. The selected text is now in the Clipboard. Paste into document and email or post to wiki.

However, I am already clear on the concept that there ought to be a GUI to capture the output and present error messages separately from the rest of the logging/progress information.

--ocat

Hum I mean to upload them onto the wiki. – fl

There is another less-travelled road, which is to segregate the mmj2 Sysout and/or Syserr messages into files using RunParms?.txt:

        *        1         2         3         4
        *234567890123456789012345678901234567890
        *CommentLine: Example #2 - default charsets="" and    
        *             new/update parameter    
        SystemErrorFile,c:\my\mmjSyserrTest001.txt,new,""    
        SystemOutputFile,c:\my\mmjSysoutTest001.txt,new,""    
      

If you specify "new" then the file must not exist – or else error! If you specify "update" the file must exist – or else error!

When using "new" add "erase" commands to your mmj2.bat file at the start:

       erase c:\my\mmjSyserrTest001.txt
       erase c:\my\mmjSysoutTest001.txt
     

Using files in this way prevents you from seeing the progress through the RunParms? but not does re-route error messages from Java itself. You might prefer to only re-route the Sysout messages and have the Syserr messages go straight to the screen…

--ocat

Hi Mel,

Thank you for your remarks about the way to re-route messages but what I would like is to upload some screenshots (.gif) ? Do you know a a way ? I think it's possible since there is the logo of Ghilbert somewhere. – fl

How to upload .gif files to wiki? No clue. Upload to somewhere else and link to them? I would be cautious about filling the asteriod with gigabytes of screen shots… --ocat

In my mind it could have been deleted a bit later. Never mind. Forget it. – fl

In answer to Ocat's question: yes, that's how you do it. As for the stated concern, IMO if you want a page with screenshots, go ahead and build it – since the images are linked in from somewhere else, it isn't a space concern here! --jcorneli
Yes but I've nowhere to store them. And what I want is to store them on this server for a short time (the time to explain Ocat what are my problems with the traces of mmj2). I know I could explain with words. That's true. – fl 5-Dec-2006

Maybe one of these would work for you?

 oh yeah ! great thank you.

I don't know if flickr allows computer-generated files…

--jcorneli

So here is my opinion about the trace (see http://www.mypicshare.com/mswihmzjpic.html) :

1 - E-PA-0403 is useless and there can be many of them since there are always several subtrees which need to be completed.

2 - In the other messages (such as E-PA-0409 and so on) the most important par of the message should be in bold (or in red …) to be identified very quickly. For instance in a distinct variable message the two variables that need to be distinct should be in bold (or in red … ).

3 - The number at the beginning of the message is not very interesting for the end user. It should be put at the end of the message. Instead at the beginning of the message there should be a visual anchor. For instance "[distinct variable]" in bold in E-PA-0409.

4 - Djvars or other technical mention is not easily understandable by the end user perhaps you could replace these mentions by some more obvious phrases.

Hoping it can help. – fl 6-Dec-2006


A user mentioned that the "ProofAsstProofFolder?" was not found, and that the RunPAGUI?.bat command was located in such and such directory…

The latest release of mmj2 provides a java "jar" file and a new Windows batch (command) file called "mmj2.bat".

The old "RunPAGUI?.bat" batch file is still retained in the release but it is used for volume/regression testing.

Please have a look at the "/mmj2/INSTALL.html" page contained in the mmj2.zip download. Specifically III.5.1, which offers my best suggestion for setting up mmj2 on your Windows machine. (The idea is to have mmj2 and metamath.exe located in the same directory so that eimm.exe has no problems finding Proof Worksheets to import/export):

     Option 5.1 -- (Recommended) Use your own private directory, such as C:\mymmj2
      
     - Create directory C:\mymmj2, and 
     
     - Copy the contents of C:\mmj2\mmj2jar into C:\mymmj2, and 
     
     - Copy the following files from C:\metamath into C:\mymmj2:
          metamath.exe
          eimm.exe
          eimmexp.cmd
          eimmimp.cmd
          set.mm (and/or whatever .mm Metamath database(s) you plan to use)
     - Update c:\mymmj2\mmj2.bat so that the PUSHD command points to
         C:\mymmj2 instead of c: \mmj2\mmj2jar
     - Update c:\mymmj2\RunParms.txt so that the ProofAsstProofFolder points
        to c:\mymmj2, as follows:
       
         ProofAsstProofFolder,C:\mymmj2
      

--ocat 25-Feb-2007


Note: Recent experiments with an iMac Mini, as well as MySQL? 5.0.27 and JAXE have given me much to consider with respect to the mmj2 "design". Obviously the user should be able to just click on something and have the product "just work" without reading anything… Not that I have a bazillion hours to redo mmj2 right now and make it all happy in multiple languages… --ocat


I have tested the new pre-release of mmj2. I have liked the clearer start message and the simplified directory structure. The parameter file seems simpler as well. I really like those simplifications very much. Installing mmj2 under linux is now very easy. – fl 1-May-2007

Thank you. I too, find it simpler using the "mmj2jar" download/ directory separate from the "mmj2" download/directory. I think that it will be best to continue in this manner with the real release – the old mmj2.zip download will be the complete version with source code, documentation, etc., and the mmj2jar.zip will be the run-only stuff (I think I should add the tutorial files to it though, to make it easy to access the PA Tutorial.)
.
I think you should continue using the pre-release version for your ongoing work, pending the final release version.
.
I now have, I believe, a clear concept of how to implement the "work variables" coding changes (at least enough for us to try out the changes and have disputes :) There are, however, two alternative algorithms, and I will attempt the simplest one first – but I have added some timing/memory instrumentation to enable me to make a proper determination of the matter. With luck and if Fate takes a brief vacation I will have something ready to test by June 1 :-)
.
--ocat 1-May-2006