mmj2 Command Line Arguments



1) New mmj2.jar Command Line Arguments


Optional path name arguments were added to the mmj2.jar command line for the mmj2,  Metamath, and mmj2 Service "home" directories. Here are the mmj2.jar command line arguments (in order):
  1. RunParm file name. This is relative to the mmj2Path directory. Mandatory.
  2. Y/N to display the new MMJ2 Fail Popup Window when startup errors and/or "fail" (abnormal termination) errors are encountered. On by default.
  3. The mmj2Path argument is used to specify mmj2 files and directories. Optional. Use "" as a placeholder if omitted -- which means use the Java Current Path as the mmj2Path.
  4. The MetamathPath argument is used to specify Metamath files -- in conjunction with RunParm "LoadFile,set.mm" and Metamath Include files referenced by the input .mm file. Optional. Use "" as a placeholder if omitted -- which means use the Java Current Path as the MetamathPath.
  5. The SvcPath argument is used to specify the SvcFolder passed as an argument in the mmj2 Service Feature (rarely used). Use "" as a placeholder if omitted -- which means use the Java Current Path as the SvcPath.

Thus, the mmj2.jar command line arguments have this format:

    java -Xincgc -Xms128M -Xmx256M -jar mmj2.jar  RunParmFileName  mmj2FailPopopWindow  mmj2Path  MetamathPath  SvcPath  ArgumentOptionsReport


The actual Windows command line from mmj2.bat is:

    java -Xincgc -Xms128M -Xmx256M -jar mmj2.jar  RunParms.txt  Y  "" c:\metamath  ""

Note: by using mmj2Path = "" the Java Current Path is used for the mmj2 data path -- and in this case the Current Path is the location of mmj2.bat, which is in the mmj2jar directory. So by using mmj2Path = "" we're making mmj2.bat portable so that no changes are required if the mmj2jar directory is moved. In fact, assuming that your set.mm file is installed at c:\metamath\set.mm after you unzip the mmj2.zip download file you can simply double-click c:\mmj2\mmj2jar\mmj2.bat to run mmj2.


In Mac OSX the Applications/Utilities/Terminal source file command line looks like this (modify it to match your system and installations -- similar in other Unix/Linux based systems):

    java -Xincgc -Xms128M -Xmx256M -jar mmj2.jar  RunParms.txt  Y  /Users/Userone/mmj2  /Users/userone/metamath  ""


For Mac OSX users an Applications/Utilities/Terminal source file named MacRunMMJ2.txt is provided. Modify it to suit your system and installations (and locate it anywhere you please), then enter the Terminal command

    source MacRunMMJ2.txt


2) RunParm File Changes

The standard RunParms.txt file was changed to be "platform agnostic" as well as friendlier and simpler for new users, as follows:

3) New "mmj2 Fail Popup Window"

Command Line Argument #2 above is the "displayMMJ2FailPopupWindow" argument.  How it works:


4) New Command Line "Argument Option" Report

Below is a sample of what you see running mmj2.bat from within the Windows Command Prompt utility.

Notice that the Argument Options Report shows the current version of mmj2.jar, including the date/timestamp -- which should match the date/timestamp of the mmj2.jar file itself.

Also, notice that the Command Line Arguments are shown twice: first as the are originally received by the program, and then again as they are interpreted -- are for each path argument, in parthenseses, an example file shows the full data path in effect.

c:\mmj2jar>mmj2

c:\mmj2jar>java -Xincgc -Xms128M -Xmx256M -jar mmj2.jar RunParms.txt Y "" c:\metamath ""


CommandLineArguments.displayArgumentOptionReport():

Hi! I am mmj2 Release 20111101 as of 15-Oct-2011 03:34.
Send mmj2 support? Paypal to siskiyousis at gmail.com
Need mmj2 help? Email x178g243 at yahoo.com.

  Command Line Arguments:
    Arg #1 = RunParms.txt
    Arg #2 = Y
    Arg #3 =
    Arg #4 = c:\metamath
    Arg #5 =

  [3] mmj2Path     = null (e.g. C:\mmj2jar\YourFile.xyz)
  [4] metamathPath = c:\metamath (e.g. C:\metamath\YourFile.xyz)
  [5] svcPath      = null (e.g. C:\mmj2jar\YourFile.xyz)
  [1] runParmFile  = c:\mmj2jar\RunParms.txt
  [2] displayMMJ2FailPopupWindow
                   = true

***END CommandLineArguments.displayArgumentOptionReport()***


**** I-UT-0015 Processing RunParmFile Command #1 = LoadFile,set.mm
**** I-UT-0015 Processing RunParmFile Command #2 = VerifyProof,*
**** I-UT-0015 Processing RunParmFile Command #3 = Parse,*
**** I-UT-0015 Processing RunParmFile Command #4 = ProofAsstUnifySearchExclude,biigb,xxxid,dummylink
**** I-UT-0015 Processing RunParmFile Command #5 = ProofAsstProofFolder,myproofs
**** I-UT-0015 Processing RunParmFile Command #6 = TheoremLoaderMMTFolder,myproofs
**** I-UT-0015 Processing RunParmFile Command #7 = RunProofAsstGUI

etc.
etc.


5) Old Command Line Arguments Eliminated:

  These new mmj2.jar command line arguments replace existing arguments which (apparently) are never used and will likely never be used by anyone, ever... (not even in the mmj2 batch/regression test kit ):



BELOW is documentation written about the new Paths arguments prior to writing code. You may find it useful or interesting, but probably not. Feel free to stop reading and ignore the rest of this document.

The Problem

mmj2 allows files to be specified using either "absolute" or "relative" paths. See http://download.oracle.com/javase/1,5.0/docs/api/java/io/File.html for an excellection discussion of absolute vs. relative path names.

Unfortunately, (with a few exceptions such as the ProofAsstProofFolder RunParm specification), the general parent of relative path names cannot be specified inside mmj2 -- and default to the Current Path (the directory from which mmj2 is being run or the path set by the "pushd" command used when running mmj2.)

As a result:


The Solution

Optional path name arguments will be added to the mmj2.jar command line (in mmj2.bat) to specify the mmj2 and the Metamath "home" directories:
Here is how a path name argument will be used. Let's use LoadFile as an example:
Example:
ARGUMENTS AND PARAMETERS___________________________________________________
FILE TO BE LOADED_________________________________
"LoadFile,c:\metamath\set.mm" "c:\metamath\set.mm"
"LoadFile,set.mm", Metamath Path Name omitted, Current Path is "c:\mmj2jar" "c:\mmj2jar\set.mm"
"LoadFile,set.mm", Metamath Path "metamath", Current Path is "c:\mmj2jar"
"c:\mmj2jar\metamath\set.mm"
"LoadFile,set.mm", Metamath Path "c:\metamath", Current Path is "c:\mmj2jar" "c:\metamath\set.mm"




Current System Data Accesses


COMMONLY USED RUNPARMS and COMMAND ARGUMENTS
WHERE_FILE_CONSTRUCTED/HOW_PATH_USED__________________________________________________________________________
java -Xincgc -Xms128M -Xmx256M -jar mmj2.jar RunParms.txt src\mmj\util\BatchFramework#runIt() calls
src\mmj\util\RunParmFile#RunParmFile() --> relative to current path

and

java -jar mmj2.jar --> current path searched first
LoadFile,c:\metamath\set.mm src\mmj\util\LogicalSystemBoss#doLoadFile() calls
src\mmj\mmio\Systemizer#load()
--> relative to current path
ProofAsstProofFolder,c:\my\proofs src\mmj\util\ProofAsstBoss#editProofAsstProofFolder() calls
src\mmj\util\Boss#editExistingFolderRunParm() calls
src\mmj\util\Boss#buildFileObjectForExistingFolder()
--> relative to current path
TheoremLoaderMMTFolder,c:\my\proofs src\mmj\util\TheoremLoaderBoss#editTheoremLoaderMMTFolder() calls
src\mmj\tl\TlPreferences#setMMTFolder() calls
src\mmj\tl\MMTFolder#MMTFolder()
--> relative to current path
LoadTheoremsFromMMTFolder,*
src\mmj\util\TheoremLoaderBoss#editLoadTheoremsFromMMTFolder() calls
src\mmj\tl\TheoremLoader#loadTheoremsFromMMTFolder() calls
src\mmj\tl\MMTFolder#constructMMTTheoremSet() calls
java.io.File.listFiles()
--> relative to MMTFolder
GMFFExportParms,althtml,ON,althtmldef,GMFF\althtml,.html,
GMFF\models\althtml,A,ISO-8859-1,general
src\mmj\util\GMFFBoss#doRunParmGMFFExportParms() calls
src\mmj\gmff\GMFFExportParms#GMFFExportParms()

and then caches the GMFFExportParms by call to

src\mmj\gmff\GMFFManager#accumInputGMFFExportParms()

then, later...
src\mmj\gmff\GMFFManager#initialization() calls
src\mmj\gmff\GMFFManager#loadExportParmsList() calls
src\mmj\gmff\GMFFManager.#validateExportParmsList() calls
src\mmj\gmff\GMFFExportParms#areExportParmsValid()

then
src\mmj\gmff\GMFFExportParms#areExportParmsValid() calls
src\mmj\gmff\GMFFExportParms#validateExportDirectory() calls
src\mmj\gmff\GMFFFolder#GMFFFolder() --> relative to current path

and
src\mmj\gmff\GMFFExportParms#areExportParmsValid() calls
src\mmj\gmff\GMFFExportParms#validateModelsDirectory() calls
src\mmj\gmff\GMFFFolder#GMFFFolder() --> relative to current path

and
src\mmj\gmff\GMFFExportParms#areExportParmsValid() calls
src\mmj\gmff\GMFFExportParms#validateOutputFileName()
--> output file name is (enforced) local file name in Export Directory.

ProofAsstGUI FILE ACCESSES

File / Save Proof File
and saveIfAskedBeforeExit()
src\mmj\pa\ProofAsstGUI#doFileSaveAction() calls
javax.swing.JFileChooser#.getSelectedFile()
--> initially relative to ProofAsstProofFolder but user can change

and
src\mmj\pa\ProofAsstGUI#doFileSaveAction() calls
saveOldProofTextFile()
--> output path and name selected/approved by user (no change required)

and
src\mmj\pa\ProofAsstGUI#doFileSaveAction() calls
saveNewProofTextFile()
--> output path and name selected/approved by user (no change required)
File / Open Proof File
src\mmj\pa\ProofAsstGUI#doFileOpenAction() calls
javax.swing.JFileChooser#.getSelectedFile()
--> initially relative to ProofAsstProofFolder but user can change

and
src\mmj\pa\ProofAsstGUI#doFileOpenAction() calls
src\mmj\pa\ProofAsstGUI#startRequestAction(new RequestFileOpen()) calls
src\mmj\pa\ProofAsstGUI#RequestFileOpen#send() calls
src\mmj\pa\ProofAsstGUI#readProofTextFromFile()
--> no change required, file chosen/approved by user
File / Save As
(basically the same as File / Save Proof File with respect to file accesses. --> no change required)
File / Export Via GMFF
GMFF / Export Via GMFF
src\mmj\pa\ProofAsstGUI#doFileExportViaGMFFAction() calls
src\mmj\pa\ProofAsstGUI#startRequestAction(new RequestExportViaGMFF()) calls
src\mmj\pa\ProofAsstGUI#RequestExportViaGMFF#send() calls
src\mmj\pa\ProofAsst#exportViaGMFF() calls
src\mmj\gmff\GMFFManager#exportProofWorksheet() calls
src\mmj\gmff\ModelAExporter#exportProofWorksheet() calls
src\mmj\gmff\GMFFExporter#outputToExportFile() calls
src\mmj\gmff\GMFFExporter#writeExportFile() calls
src\mmj\gmff\GMFFExportFile#GMFFExportFile()
--> relative to gmffExportParms.exportFolder (no change required)

also

src\mmj\gmff\GMFFExporter#readModelFile() calls
src\mmj\gmff\GMFFInputFile#GMFFInputFile()
--> relative to gmffExportParms.modelsFolder (no change required)

also
src\mmj\gmff\GMFFManager#exportProofWorksheet() calls
src\mmj\gmff\GMFFManager#initialization() calls
src\mmj\gmff\GMFFManager#loadExportParmsList() calls
src\mmj\gmff\GMFFManager.#validateExportParmsList() calls
src\mmj\gmff\GMFFExportParms#areExportParmsValid()

and
src\mmj\gmff\GMFFExportParms#areExportParmsValid() calls
src\mmj\gmff\GMFFExportParms#validateExportDirectory() calls
src\mmj\gmff\GMFFFolder#GMFFFolder() --> relative to current path

and
src\mmj\gmff\GMFFExportParms#areExportParmsValid() calls
src\mmj\gmff\GMFFExportParms#validateModelsDirectory() calls
src\mmj\gmff\GMFFFolder#GMFFFolder() --> relative to current path

and
src\mmj\gmff\GMFFExportParms#areExportParmsValid() calls
src\mmj\gmff\GMFFExportParms#validateOutputFileName()
--> output file name is (enforced) local file name in Export Directory.
TL / Unify + Store In LogSys and MMT Folder
src\mmj\pa\ProofAsstGUI#startUnificationAction(
      false, null, null, new StoreInLogSysAndMMTFolderTLRequest()) calls
src\mmj\tl\TheoremLoader#storeInLogSysAndMMTFolder() calls
src\mmj\tl\TheoremLoader#storeInMMTFolder() calls
src\mmj\tl\MMTFolder#storeMMTTheoremFile() calls
src\mmj\tl\MMTTheoremFile#MMTTheoremFile()
--> relative to MMTFolder (no change required)

and
src\mmj\tl\TheoremLoader#storeInLogSysAndMMTFolder() calls
src\mmj\tl\TheoremLoader#loadTheoremsFromMMTFolder() calls
src\mmj\tl\MMTFolder#constructMMTTheoremSet() calls
java.io.File#listFiles()
--> relative to MMTFolder (no change required)

and
src\mmj\tl\MMTFolder#constructMMTTheoremSet() calls
src\mmj\tl\MMTTheoremSet#MMTTheoremSet()
--> relative to MMTFolder (no change required)
TL / Unify + Store In MMT Folder (basically the same as TL / Unify + Store In LogSys
and MMT Folder with respect to file accesses)
TL / Load Theorems From MMT Folder
src\mmj\pa\ProofAsstGUI#doLoadTheoremsFromMMTFolderItemAction() calls
src\mmj\pa\ProofAsstGUI#startRequestAction(new RequestLoadTheoremsFromMMTFolder()) calls
src\mmj\pa\ProofAsst#loadTheoremsFromMMTFolder() calls
src\mmj\tl\TheoremLoader#loadTheoremsFromMMTFolder() calls
src\mmj\tl\MMTFolder#constructMMTTheoremSet() calls
java.io.File.listFiles() --> relative to MMTFolder
TL / Extract Theorem To MMT Folder
src\mmj\pa\ProofAsstGUI#doExtractTheoremToMMTFolderItemAction() calls
src\mmj\pa\ProofAsstGUI#startRequestAction(new RequestExtractTheoremToMMTFolder) calls
src\mmj\pa\ProofAsst#extractTheoremToMMTFolder() calls
src\mmj\tl\TheoremLoader#extractTheoremToMMTFolder() calls
src\mmj\tl\MMTFolder#storeMMTTheoremFile() calls
java\src\mmj\tl\MMTTheoremFile#MMTTheoremFile()
--> relative to MMTFolder (no change required)
TL / Set Theorem Loader MMT Folder
src\mmj\pa\ProofAsstGUI#doSetTLMMTFolderItemAction() calls
src\mmj\pa\ProofAsstGUI#getNewMMTFolder() calls
javax.swing.JFileChooser#getSelectedFile()
--> chosen/approved by user (no change needed)
ProofAsstGUI constructor (start-up)
src\mmj\pa\ProofAsstGUI#ProofAsstGUI() calls
src\mmj\pa\ProofAsstGUI#buildFileChooser()
--> relative to ProofAsstProofFolder (no change required)


USED IN BATCH/REGRESSION TESTING

UnifyPlusStoreInMMTFolder,c:\myproofs\syl.mmp src\mmj\util\TheoremLoaderBoss#editUnifyPlusStoreInMMTFolder() calls
src\mmj\util\ProofAsstBoss#editProofAsstImportFileRunParm() calls
src\mmj\util\Boss#doConstructBufferedFileReader()
--> relative to ProofAsstProofFolder (no change needed!)

then ...

src\mmj\tl\TheoremLoader#unifyPlusStoreInMMTFolder() calls
src\mmj\tl\TheoremLoader#storeInMMTFolder() calls
src\mmj\tl\MMTFolder#storeMMTTheoremFile() calls
src\mmj\tl\MMTTheoremFile#MMTTheoremFile()
--> relative to MMTFolder (no change needed)
UnifyPlusStoreInLogSysAndMMTFolder,c:\myproofs\syl.mmp src\mmj\util\TheoremLoaderBoss#editUnifyPlusStoreInLogSysAndMMTFolder() calls
src\mmj\util\ProofAsstBoss#editProofAsstImportFileRunParm() calls
src\mmj\util\Boss#doConstructBufferedFileReader()
--> relative to ProofAsstProofFolder (no change needed!)

then...

src\mmj\util\TheoremLoaderBoss#editUnifyPlusStoreInLogSysAndMMTFolder() calls
src\mmj\tl\TheoremLoader#unifyPlusStoreInLogSysAndMMTFolder() calls
src\mmj\tl\TheoremLoader#storeInLogSysAndMMTFolder() calls
src\mmj\tl\TheoremLoader#storeInMMTFolder() calls
src\mmj\tl\MMTFolder#storeMMTTheoremFile() calls
src\mmj\tl\MMTTheoremFile#MMTTheoremFile()
--> relative to MMTFolder (no change needed)
ExtractTheoremToMMTFolder,syl
src\mmj\util\TheoremLoaderBoss#editExtractTheoremToMMTFolder() calls
src\mmj\tl\TheoremLoader#extractTheoremToMMTFolder() calls
src\mmj\tl\MMTFolder#storeMMTTheoremFile() calls
java\src\mmj\tl\MMTTheoremFile#MMTTheoremFile()
--> relative to MMTFolder (no change required)
ProofAsstExportToFile,*,c:\my\export.mmp,new,un-unified,Randomized,Print,NoDeriveFormulas src\mmj\util\ProofAsstBoss#doProofAsstExportToFile() calls
src\mmj\util\ProofAsstBoss#editProofAsstExportFileRunParm() calls
src\mmj\util\Boss#doConstructBufferedFileWriter()
--> relative to ProofAsstProofFolder (no change required)
ProofAsstBatchTest,*,c:\my\export.mmp,un-unified,NotRandomized,
NoPrint,DeriveFormulas,NoCompareDJs,NoUpdateDJs,NoAsciiRetest
src\mmj\util\ProofAsstBoss#doProofAsstBatchTest() calls
src\mmj\util\ProofAsstBoss#editProofAsstImportFileRunParm() calls
src\mmj\util\Boss#doConstructBufferedFileReader()
--> relative to ProofAsstProofFolder (no change required)
StepSelectorBatchTest,c:\mmj2\UT7000.mmp,326,6 src\mmj\util\ProofAsstBoss#doStepSelectorBatchTest() calls
src\mmj\util\ProofAsstBoss#editProofAsstImportFileRunParm() calls
src\mmj\util\Boss#doConstructBufferedFileReader()
--> relative to ProofAsstProofFolder (no change required)
PreprocessRequestBatchTest,C:\mmj2\data\mmp\tests\UT7001.mmp,EraseAndRederiveFormulas
src\mmj\util\ProofAsstBoss#doPreprocessRequestBatchTest() calls
src\mmj\util\ProofAsstBoss#editProofAsstImportFileRunParm() calls
src\mmj\util\Boss#doConstructBufferedFileReader()
--> relative to ProofAsstProofFolder (no change required)
GMFFExportFromFolder,myproofs,syl,.mmp,999999,AppendFileName
src\mmj\util\GMFFBoss#doGMFFExportFromFolder() calls
src\mmj\gmff\GMFFManager#exportFromFolder() calls
src\mmj\gmff\GMFFFolder#GMFFFolder()
--> relative to current path

and

src\mmj\gmff\GMFFManager#exportFromFolder() calls
src\mmj\gmff\GMFFManager#exportProofWorksheet() calls
src\mmj\gmff\ModelAExporter#exportProofWorksheet() calls
src\mmj\gmff\GMFFExporter#outputToExportFile() calls
src\mmj\gmff\GMFFExporter#writeExportFile() calls
src\mmj\gmff\GMFFExportFile#GMFFExportFile()
--> relative to gmffExportParms.exportFolder (no change required)

(note: append file...always just a local file name, not a path name)
GMFFExportTheorem,syl,999999,AppendFileName src\mmj\util\GMFFBoss#doGMFFExportTheorem() calls
src\mmj\gmff\GMFFManager#exportTheorem() calls
src\mmj\gmff\GMFFManager#gmffExportOneTheorem() calls
src\mmj\gmff\GMFFManager#exportProofWorksheet() calls
src\mmj\gmff\ModelAExporter#exportProofWorksheet() calls
src\mmj\gmff\GMFFExporter#outputToExportFile() calls
src\mmj\gmff\GMFFExporter#writeExportFile() calls
src\mmj\gmff\GMFFExportFile#GMFFExportFile()
--> relative to gmffExportParms.exportFolder (no change required)

(note: append file...always just a local file name, not a path name)
GMFFParseMetamathTypesetComment,althtmldef,mydirectory,
mytypesetdefs.mm,PRINT
src\mmj\util\GMFFBoss#doGMFFParseMetamathTypesetComment() calls
src\mmj\gmff\GMFFManager#parseMetamathTypesetComment() calls
src\mmj\gmff\GMFFFolder#GMFFFolder()
--> relative to current path (note: should be modified to use mmj2Path)

and

src\mmj\gmff\GMFFManager#parseMetamathTypesetComment() calls
src\mmj\gmff\GMFFInputFile#getFileContents()
--> mytypesetdefs.mm is relative to mydirectory (expected to be a
local file name in that directory)


INFREQUENTLY USED

SystemErrorFile,c:\my\mmjSyserrTest001.txt,new,"" src\mmj\util\OutputBoss#editSysErrFile() calls
src\mmj\util\Boss#editPrintWriterRunParm() calls
src\mmj\util\Boss#doConstructPrintWriter()
--> relative to current path
SystemOutputFile,c:\my\mmjSysoutTest001.txt,new,""
src\mmj\util\OutputBoss#editSysOutFile() calls
src\mmj\util\Boss#editPrintWriterRunParm() calls
src\mmj\util\Boss#doConstructPrintWriter()
--> relative to current path
ProofAsstStartupProofWorksheet,c:\mmj2\data\mmp\PATutorial\Page101.mmp src\mmj\util\ProofAsstBoss#editProofAsstStartupProofWorksheet() calls
src\mmj\util\Boss#editExistingFileRunParm() calls
java\src\mmj\util\Boss#buildFileObjectForExistingFile()
--> relative to current path
SvcFolder,c:\my\java\test\mmj\svc src\mmj\util\SvcBoss#editSvcFolder() calls
src\mmj\util\Boss#editExistingFolderRunParm() calls
src\mmj\util\Boss#buildFileObjectForExistingFolder()
--> relative to current path
Metamath Include File
src\mmj\util\LogicalSystemBoss#doLoadFile() calls
isInFilesAlreadyLoaded()
--> relative to current path
(and
src\mmj\mmio\Systemizer#initIncludeFile() calls
src\mmj\mmio\IncludeFile#initIncludeFile()
to actually construct the Reader using a File)