mmj2 Installation

//********************************************************************/

//* Copyright (C) 2005 - 2011           
                           
*/

//* MEL O'CAT  : x178g243 at yahoo.com      
  
                    
*/

//* License terms: GNU General Public License Version
2             
*/

//*               
or
any
later
version                             
*/

//********************************************************************/

//*4567890123456 (71-character line to adjust editor window) 23456789*/

As Of 1-Nov-2011 Release

Preliminary Remarks:

WARNINGS:

Back up your data before attempting any of this stuff!
These instructions are believed to be useful but are not guaranteed -- and none of the software mentioned here is guaranteed either!
Backup your data and be prepared for the absolute worst case scenario, a complete System Restore!

1. This document is customized for Windows. The batch files (".bat") provided in mmj2 to compile the source code and javadoc include commands available on Windows XP (such as "call") that may not be present on older versions of Windows. mmj2 has been used on Linux systems without difficulty.

2. Both source code and an executable Java "jar" file are included. It should not be necessary for you to recompile the software, but the compilation process is simple using the .bat command files provided.

3. You will likely need at least 256MB of RAM and a modern hard drive that is fairly speedy in order to have a satisfactory experience.

4. You will need Sun's Java 2 platform, release 1.5 or higher -- or an equivalent, compatible implementation of Java, including the Java "Swing" packages which are used in the mmj2 Proof Assistant GUI.

5. If you do not plan to recompile the source code for mmj2 then you will require only the Java "JRE" (Java Runtime Environment) which is available here:

Java Runtime Environment Version 6.0 Update 26 (as of 1-Jul-2011)
http://www.oracle.com/technetwork/java/javase/downloads/jre-6u26-download-400751.html

6. If you do plan to recompile the source code for mmj2 then download the current production version -- "JDK 5.0" -- which is also referred to by Sun as "

J2SE
1.5.0

" (I know, it is confusing...) This download includes the JRE as well, (so it is not necessary to separately download the Java JRE if you download the JDK.) Available here:

JDK 6.0 Update 26 -- The Java SE Development Kit (JDK)
http://www.oracle.com/technetwork/java/javase/downloads/jdk-6u26-download-400750.html

7. Regardless of whether you plan to use the JDK (which includes the JRE) or just the JRE, it is recommended that you upgrade to the current version of the Java software so that any Sun Microsystems Inc. bug fixes are implemented on your system.

8. Also, you will surely need, if you don't already have one, a good text editor that can handle not only large files but also the Metamath-friendly Unix-style line endings (Win/DOS text files are terminated with CR-LF, Carriage-return and Line-feed while Unix files are terminated with just CR.) This might work well for you, try an evaluation of:

http://www.textpad.com/

9. Finally, you will want to download Metamath (more on this below):

http://www.metamath.org/

10. Recommendation: One approach is to store all downloaded software packages in a separate C:\downloads directory, with a separate subdirectory for each package. This allows for simple periodic backup of all downloaded software, which is very convenient when the time comes to migrate to a new machine -- or following a system restore. It is also a handy way to stay organized. And when it comes time to reinstall with a new copy of Metamath or mmj2, which are basically just ".zip" files, it is convenient to create a "temp" sub-subdirectory within the package's subdirectory, unzip to "..\temp", and then copy the contents of the unzipped directories to the previous install location. (In the future you might need to install just the mmj2jar.jar file, and perhaps update your RunParms file when a new release or patch of mmj2 is produced.)

I. INSTALL Metamath

Go to http::\www.metamath.org, and visit the download page. Follow the instructions there. It is simple.

You will want to download the following download files, at least:

Metamath.pdf
Metamath.zip (contains set.mm too)
eimm.zip

FYI, Metamath.zip is just a directory. "Install" it by just unzipping it to the "C" drive, which creates directory "c:\metamath". And that's it for that...unless you want to add "c:\metamath" to the Windows environment "path" (see II below).

The mmj2.zip download provides certain handy .bat files, including these that build html pages:

C:\mmj2\test\windows\cr_althtml.bat
C:\mmj2\test\windows\cr_brief_althtml.bat

You need to start up a Command Prompt window and then "CD" -- Change Directory -- to the destination directory, "c:\metamath" before running them:

cd c:\matamath

II. INSTALL Java JDK/JRE or just JRE

You will need Sun's Java 2 platform, release 1.5 or higher -- or an equivalent, compatible implementation of Java, including the Java "Swing" packages which are used in the mmj2 Proof Assistant GUI.

I recommend choosing their "Offline Installation" option, which gives you an ".exe" download file that you execute to install Java. The advantage is that you can back up the installation file in case it is needed again.

If you do not plan to recompile the source code for mmj2 then you will require only the Java "JRE" (Java Runtime Environment) which is available here:

Java Runtime Environment Version 6.0 Update 26 (as of 1-Jul-2011)
http://www.oracle.com/technetwork/java/javase/downloads/jre-6u26-download-400751.html

If you do plan to recompile the source code for mmj2 then download the current production version -- "JDK 5.0" -- which is also referred to by Sun as "

J2SE
1.5.0

" (I know, it is confusing...) This download includes the JRE as well, (so it is not necessary to separately download the Java JRE if you download the JDK. Available here:

JDK 6.0 Update 26 -- The Java SE Development Kit (JDK)
http://www.oracle.com/technetwork/java/javase/downloads/jdk-6u26-download-400750.html

Regardless of whether you plan to use the JDK (which includes the JRE) or just the JRE, it is recommended that you upgrade to the current version of the Java software so that any bug fixes are implemented on your system.

Follow Sun's installation instructions. It is actually very simple for a plain-vanilla install. What it boils down to is running their .exe install program (after first un-installing if you have a previous version of Java), and then updating your Windows "Path" variable:

Click Start,
then Settings,
then Control Panel,
then System
then Advanced
then Environment Variables
and update the Path variable by inserting C:\Program Files\Java\jdk1.5.0_06\bin;

(Change that to reflect the location and name of the "bin" directory of your JDK or JRE -- and it may be that Sun has already put it there so just double-check for yourself before doing anything!)

You will probably want to download the Java documentation along with the JDK. It is just a zip file of their "doc" directory. Unzip it to the top level directory of the JDK:

C:\Program
Files\Java\jdk1.5.0_06\

(change that name to reflect the version you installed)

Unzip will create a "doc" directory at the same level as "bin".

III. INSTALL mmj2:

NOTE: short-cut Windows instructions: 1) download mmj2.zip; 2) unzip it to c:\mmj2; 3) copy c:\mmj2\mmj2jar to create c:\mmj2jar. Then in a Command Prompt window at c: prompt, to run mmj2, enter command "cd mmj2jar" followed by command "mmj2.bat" (or just "mmj2").

1. Download mmj2 from:

http://us2.metamath.org:8888/ocat/mmj2/

This is the whole package:

http://us2.metamath.org:8888/ocat/mmj2/mmj2.zip

An MD5 checksum file is available at

http://us2.metamath.org:8888/ocat/mmj2/mmj2.md5

Use the MD5 checksum to confirm the integrity and non-hacked status of mmj2.zip -- and of course virus-scan any downloaded files before touching them with any other software!


2. Unzip "mmj2.zip" to the "C" drive, thus creating
   top-level directory:

        c:\mmj2

NOTE: If you use a different drive letter or directory name then several mmj2 .bat files and parameter files will need to be updated -- run a scan to see which need the fix...

For more info see:
        C:\mmj2\doc\MMJ2DirectoryStructure.txt

3. Compile the mmj2 source code.

Note: if you plan to use the executable mmj2 code provided in the mmj2.zip download file then skip Steps 3 and 4 (Steps 3 and 4 require the Java JDK download from Sun, whereas just running mmj2 requires only the Java JRE download.)

- Venture to a Windows Command Prompt (at Start/Programs/Accessories/Command Prompt -- I recommend that you right-mouse click the Command Prompt menu item and select "

Create
Shortcut

" so that a Command Prompt desktop icon is conveniently available on the Windows desktop for future use.)

- If you got mmj2 from git, enter this command to get code which mmj2 depends on:

        git submodule init

        git submodule update

- Enter this command to compile the mmj2 source code:

C:\mmj2\compile\windows\CompMMJ.bat

- Note: this .bat file creates the c:\mmj2\mmj2jar\mmj2jar.jar file, in addition to creating the various mmj2 class files.

4. Compile the Javadoc for mmj2.

- Use the Command Prompt window to execute the following command:

C:\mmj2\doc\windows\BuildDoc.bat

5. Choose and create a personal, private directory for doing mmj2 and Metamath activities. This is where you will store proofs and any customized RunParm files, as well as copies of the executable software for mmj2 and Metamath.

Note: The directory c:\mmj2\mmj2jar contains the mmj2jar.jar executable file plus a .txt RunParms file designed to work "out of the box" with Metamath's set.mm Metamath database (see AnnotatedRunParms.txt for details of RunParms.). Directory c:\mmj2\mmj2jar contains what you need to actually run mmj2 -- the rest of the c:\mmj2 directory consists of documentation, test files and other items that may be of greater or lesser interest to you, depending on your interests and intentions.

There are two main possibilities: 5.1 Create your own directory, or, 5.2 Do your work inside the C:\metamath directory. The Metamath eimm.exe (Export/Import mmj2 Proof Worksheets) program requires that it be located inside the current directory, along with its helpers eimmexp.cmd and eimmimp.cmd. Therefore, if you plan to use mmj2 and Metamath with Metamath's eimm.exe utility, it is simplest to have all of the software in a single directory.

Option 5.1 -- (Recommended) Use your own private directory, such as C:\mmj2jar

- Copy the contents of C:\mmj2\mmj2jar to create C:\mmj2jar

- Copy the following files from C:\metamath into C:\mmj2jar

metamath.exe
eimm.exe
eimmexp.cmd
eimmimp.cmd
set.mm (and/or whatever .mm Metamath database(s) you plan to use)

- - 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

- Note: if you choose to store set.mm elsewhere, remember to update the mmj2jar\RunParms.txt file's LoadFile RunParm to point to the correct location!

Option 5.2 (Also good) -- Do your work inside the C:\metamath directory

- Copy the contents of C:\mmj2\mmj2jar into C:\metamath, and

- 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

- Note: RunParms.txt file's LoadFile RunParm refers to set.mm.

6. Running It.

In the Windows Explorer program, double-click the c:\mmj2jar\mmj2.bat file.

OR

As a test to confirm that mmj2 has been installed correctly go to a Command Window and run the following commands to start the mmj2 Proof Assistant Tutorial:

Microsoft Windows XP [Version blahblah]
(C) Copyright 1985-2001 Microsoft Corp.

C:\>cd c:\mmj2jar

C:\mmj2jar>mmj2PATutorial.bat

Refer to the Proof Assistant User Guide and mmj2.html for more information