cmd windowHere is how you run mmj2 and the Proof Assistant (see footnote at end of page):
(back to Start.html)
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 |
Microsoft Windows XP [Version
blahblah] (C) Copyright 1985-2001 Microsoft Corp. C:\>cd mmj2jar C:\mmj2jar>mmj2 |
Microsoft Windows XP [Version
blahblah] (C) Copyright 1985-2001 Microsoft Corp. C:\>cd mmj2jar C:mmj2jar>mmj2PATutorial |
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.)mmj2jar
")..bat
" portion of the "mmj2.bat
" name is
optional. Windows can figure out the missing
".bat
" part of the name.mmj2.bat
file name
-- which
works, except that the system error messages will disappear when the
program ends.)BatchMMJ2
",
which are rarely used and need not be documented here.)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:
MaxErrorMessages
MaxInfoMessages
LoadComments
LoadProofs
LoadEndpointStmtNbr
LoadEndpointStmtLabel
(back to Start.html)