//* Copyright (C) 2005 thru 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

For Info about the latest release features click on:
See also: QuickStart.html  And README.html

You can now support mmj2 development with $$$ donations via Paypal to siskiyousis at gmail.com!

And, for questions, bugs, enhancements, etc. contact Mel at X178G243 at yahoo.com

    Quick Start CHEAT SHEET!!!  (see also mmj2\QuickStart.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
       (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.)

mmj2 The key idea of mmj2 and its Proof Assistant -- why you want it --  is that it has a "GUI" Proof Assistant which is said to be much easier to use than Metamath.exe.

mmj2 provides a set of tools designed for use with Metamath.exe and its associated utilities, such as eimm.exe (Import/Export mmj2 Proof Worksheet). In addition to the new and improved mmj2 Proof Assistant GUI -- by far, the most interesting and useful part of mmj2 -- the mmj2 software package provides capabilities such as validation of .mm files; proof verification; grammatical/syntax analysis of .mm files; printing; Text Mode Formula Formatting  ("TMFF"), a novel "pretty printing" feature that may facilitate comprehension of complicated math and logic formulas written in Metamath's ASCII shorthand; and MUCH MORE...

1. Installation: Refer to INSTALL.html for instructions on installing and taking the next steps to run and use mmj2. Then visit or return to mmj2.html to see the other documentation, such as the mmj2 Proof Assistant User Guide. Once you have installed mmj2 be sure to try the interactive mmj2 Proof Assistant Tutorial (which ought to take about an hour.)

2. Requirements:

3. Limitations:  mmj2 is still in "developmental" status, meaning that it is subject to change, bug fixes and continuing enhancements...at the whim of Mel L. O'Cat (If you don't like the changes you can clone mmj2 under the GNU GENERAL PUBLIC LICENSE and write your own code.) There is NO WARRANTY -- see LICENSE.TXT (GNU GENERAL PUBLIC LICENSE Version 2, June 1991). Use at your own risk. (In any case, you are strongly urged to always backup your data; to secure your machine from hackers and viruses, whether or not you use mmj2; to feed your PC only clean electricity from a battery-powered UPS; and ... to always remember that the only secure computer is one that is unplugged, re-packed in its original shipping container, and safely stacked in a secure warehouse. I recommend using a firewall such as Norton which allows you to specify which programs are allowed to access the internet -- and then to block Java from internet access...better yet, disconnect your computer from the internet while you are using mmj2 :-) Better safe than sorry!)

4. Opportunities: mmj2 was begun as an experimental study of Metamath, and development has proceed in stages, with each new enhancement package designed to be as modular and independent from the others as possible. These developmental stages -- from .mm database validation and printing, proof verification, grammatical analysis, "proof assistanting", Text Mode Formula Formatting, etc. -- have advanced the state of  the art of Metamath programming by a small amount and provide a foundation for further work. mmj2 is now usable (and almost good enough to throw away and rewrite properly!) But there is still more work, more experimentation and more learning to be done. 

mmj2's capabilities are invoked using "RunParm" commands that form a language, albeit without looping or "if" statements. Thus, it is easy to enhance and extend mmj2, even for "one offs": code a new program, a new "RunParm" command or two, and modify the mmj.util.BatchMMJ2.java program, and one can immediately gain programmatic access to a fully parsed, proof-verified Metamath database loaded into memory and ready for use. (Note: the MMJ2 Service Feature allows your program to call mmj2 or to be called by mmj2.)

5. Shortcomings of mmj2:

6. Next Steps, Possible Enhancements, and Experimental Topics:

7. Acknowledgements: