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