cmd window

(back to Start.html)
Here is how you run mmj2 and the Proof Assistant (see footnote at end of page):
#1
Microsoft Windows XP [Version blahblah]
(C) Copyright 1985-2001 Microsoft Corp.

C:\>cd mmj2jar

C:\mmj2jar>java -Xincgc -Xms64M -Xmx128M -jar mmj2.jar RunParms.txt

Or like this:
#2
Microsoft Windows XP [Version blahblah]
(C) Copyright 1985-2001 Microsoft Corp.

C:\>cd mmj2jar

C:\mmj2jar>mmj2

And the mmj2 Proof Assistant Tutorial -- interactive -- can be run like this:
Microsoft Windows XP [Version blahblah]
(C) Copyright 1985-2001 Microsoft Corp.

C:\>cd mmj2jar

C:mmj2jar>mmj2PATutorial


Those examples assume that we have first entered a "Command Window" and that we have created directory called "c:\mmj2jar" and copied the contents of "c:\mmj2\mmj2jar" into our new mmj2jar directory. (Fyi: the "cd" command stands for "Change Directory"; hit Enter after entering a command; type "exit" and hit Enter to leave the Command Window.)

"RunParms.txt" contains commands to start mmj2 and the Proof Assistant and should be located in our directory (i.e. "mmj2jar").

In #2, typing the ".bat" portion of the "mmj2.bat" name is optional. Windows can figure out the missing ".bat" part of the name.

"Command Window" in Windows refers to a screen that allows the user to enter commands. It is shown on the Windows Desktop as an icon labelled "Command Prompt". To put a Command Prompt icon on your Desktop:
  1. Left-mouse click "Start"
  2. Left-mouse click "Programs"
  3. Left-mouse click "Accessories"
  4. Right-mouse click "Command Prompt"
  5. Left-mouse click "Create Shortcut".
Whew. That was easy. Not :)

A similar "command line" is available in other operating systems, like Linux. In fact, the "Command Prompt" is a descendant of the old (pc) DOS screen, and most of the old DOS commands still work there (even "help" :)

It is important to start mmj2 from a Command Window so that any error messages that result can be seen. If there is a problem, the output error messages are essential. (The alternative is to use Windows Explorer and just double-click on the mmj2.bat file name -- which works, except that the system error messages will disappear when the program ends.)

That is pretty much all there is to it (two other command line arguments are passed to the main program inside mmj2.jar, "BatchMMJ2", which are rarely used and need not be documented here.)

When mmj2 runs it will display the RunParm commands as it processes them, which can be interesting and helpful to watch. If a "bug" is encountered some very weird and technical looking messages will be output. Make a copy of the text of these weird looking messages to assist in debugging (this should not happen but if it does, you know what to do: report the problem at the Asteroid!)

* * *

Usage Note as of 19-Oct-2006:

Torture testing of the mmj2 Proof Assistant GUI revealed a situation that triggered an "Out of Memory" error and/or a "Out of Heap Space".

Diagnosis: we have means, motive and opportunity -- and a body -- but no actual smoking gun and signed confession... The code and java parameter changes described below prevent a recurrence of the symptoms, at least temporarily...

HOWEVER...

I strongly recommend upgrading to the Jave Runtime Environment 1.5.0_09 due to a number of Sun bug fixes pertaining to Garbage Collection. (Version 1.5.0_05 was the latest version back on 4/1/2006, so you can just imagine the exciting bee hive of activity at Java HQ :)

I have not yet upgraded my own software so if you upgrade now and report back to the Asteroid you will be performing a service to mmj2 and your fellow users...

ALSO...

The following executive actions were taken:

1) The new TMFF coding was modified for efficiency and to avoid using a suspect portion of the Java Runtime Environment.

2) New arguments on the "java" command line in mmj2.bat were added. The new command to trigger mmj2 and the Proof Assistant looks like this (inside mmj2.bat):

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

    
* The "-Xincgc" argument says "enable incremental Garbage Collection", which is off by default. Essentially what that means is to keep memory tidy as you go instead of the more typical periodic cleanliness :) Incremental Garbage Collection is less efficient and adds a small amount of time to the start-up process. But the potential payoff is that for the GUI, we won't notice an extra 1/10 second here and there and we benefit from avoiding having Java get into a stressed out condition where bad things can happen...

* The "-Xms64M" argument means that 64 MB of memory is requested as an initial allocation. Apparently, loading set.mm withComments and firing up the mmj2 Proof Assistant GUI requires 33MB -- with the 9/14/2006 version of set.mm, which is growing by 5 theorems a day :) It is best to ask for and receive a nice, juicy contiguous chunk of memory right at the start, if you have enough RAM in your computer.

* The "-Xmx128M" argument means that the Maximum memory allowed is 128 MB, which ought to be enough for the next few years of set.mm development. This amount of memory may or may not be allocated, and even if allocated may be swapped out. The Java default maximum is 64MB, and when that limit is reached and there is no free memory, processing stops.

NOTE: another interesting Java argument is "-verbose:gc". Add that *temporarily* to your mmj2.bat java command to see every action taken by the Java Garbage Collector. The activities are printed on the Command Prompt Window. (Remove the argument later as it slows things down...)

3) The Help/About menu item (which is new) has been modified to run a full Garbage Collection "sweep" just before it displays the memory utilization statistics. This is interesting and useful information -- if you need it you will want it :)

AND...

Note:

Memory utilization can be reduced using the following RunParms:
Refer to AnnotatedRunParms.txt for infomation about using these RunParms and their option values.
(back to Start.html)