Quick Start                            (see also: README)

CLICK WINDOWS or APPLE/Mac OS-X


    -----------------------------------------------------------------
    Quick Start CHEAT SHEET!!!  (see also mmj2\README.html)
    -----------------------------------------------------------------   

       Quick Start!!!:
      
       Windows:  Double-click mmj2\mmj2jar\mmj2.bat in Windows Explorer
      
       Mac OS-X: Double-click mmj2\mmj2jar\MacMMJ2.command in Finder


       BUT...WAIT!...before running mmj2, edit, if needed:

       EDIT-->Windows    mmj2\mmj2jar\RunParms.txt
              using      mmj2\mmj2jar\mmj2.bat
              Notepad:   mmj2\mmj2jar\mmj2PATutorial.bat

           -->Mac OS-X   mmj2\mmj2jar\RunParms.txt
              using      mmj2\mmj2jar\MacRunParmsPATutorial.txt                
              TextEdit:  mmj2\mmj2jar\MacMMJ2.command
                         mmj2\mmj2jar\MacMMJ2PATutorial.command
 
       (Double-click works well now because the new "mmj2 Fail Popup
       Window" *not only* provides start-up and "fail" error
       messages, but it also forces the Windows Command Prompt (Mac
       OS-X utilities\terminal.app) window to stay open, which makes
       it possible to see all of the mmj2 output about the error.)



(Copied from Norm's writing in BottomUpProving-ByNormMegill and then slightly adjusted):

WINDOWS USERS:
I'll start at the beginning, assuming you are using Windows, so you won't have to read the mmj2 documentation.  Download the latest mmj2.zip and put it in c:\mmj2.zip.  Extract the Zip file to create c:\mmj2 with default settings.  From the result, move or copy the directory c:\mmj2\mmj2jar to c:\mmj2jar (run c:\mmj2\mmj2jar\copymmj2jar.bat to create and copy c:\mmj2jar -- see below for instructions on running a ".bat" file.)

I assume you have Java installed.  If not, I guess you'll have to read the mmj2 documentation after all.

Next, download set.mm (6MB) into the directory c:\metamath.  Or, if you want it somewhere else, change the parameter

  LoadFile,set.mm

accordingly, using a text editor like Notepad to edit

   c:\mmj2jar\RunParms.txt

You may need to update the mmj2Path and MetamathPath arguments in mmj2.bat (command line arguments #3 and 4 after "mmj2.jar" -- see mmj2CommandLineArguments) in:

   c:\mmj2jar\mmj2.bat

Then double-click the c:\mmj2jar\mmj2.bat file in Windows Explorer

OR

Start a session of Windows Accessories/Command Prompt and enter:

   cd c:\mmj2jar

Then enter

   mmj2



APPLE USERS: In Mac OS-X

Download the latest mmj2.zip and put it in /Users/userone  -- substituting your directory name for "userone".

Extract the Zip file to create /Users/userone/mmj2 with default settings. 

I assume you have Java installed.  If not, download it from Apple. Or Oracle. Follow their instructions.

Next, download set.mm (6MB) into the directory /Users/userone/metamath.  Or, if you want it somewhere else, change the parameter

  LoadFile,set.mm

accordingly, using TextEdit.app to edit

  /Users/userone/mmj2/mmj2jar/RunParms.txt

You will need to update the mmj2Path and MetamathPath arguments in MacMMJ2.command (command line arguments #3 and 4 after "mmj2.jar" -- see mmj2CommandLineArguments) in:

  /Users/userone/mmj2/mmj2jar/MacMMJ2.command

 
and while you're doing this, update this one too:

  /Users/userone/mmj2/mmj2jar/MacPATutorial.command


Then  double-click the /Users/userone/mmj2/mmj2jar/MacMMJ2.command file in the Finder window