Design info uploaded for new GMFF enhancement proposal. UPDATED w/info about the Model files for GMFF…plus tweaked versions of syl.html in the \html and \althtml directories.

Let me know what you think!

See the README.html file in

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

--ocat (25-Jul-2011).

—

New version of mmj2 uploaded: Release 20110701!

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

= 3.6MB

Refer to mmj2\CHGLOG.TXT in the mmj2.zip downwload for a description of the changes.

The mmj2\README.html file also contains valuable contact information for mmj2 support, including info about logging onto this wiki as an editor.

A few interesting topics :-)

- You can now support mmj2 development with monetary donations via Paypal to siskiyousis at gmail.com! Continuing maintenance and new enhancements (Jan 2012?) are time-consuming and way more than 1000 hours of work have already been invested in mmj2.

- The new release contains mmj2\data\mm\RegressionTest?1set.mm which is a snapshot of the 20-Aug-2008 set.mm. This file will be used for regression testing of new software releases going forward. The problem this solves is that over time a large number of symbols and statement labels in set.mm change and updating the mmj2 test data to match is too much work.

- Since 2008 the number of symbols and statements in set.mm have increased by enough to justify increasing memory allocations in the mmj2.bat file. A Total Memory size of 128MB and a Maximum Memory equal to 256MB are specified.

--ocat 6-Jul-2011

— mmj2 is an open source software package for use with metamath (.mm) databases. It is written in Java and provides both batch (command line) and GUI capabilities. Its most notable feature is the mmj2 Proof Assistant GUI, which provides support for Metamath proof development and is perhaps easier to use than the metamath.exe proof assistant (note: power users benefit from using both proof assistants simultaneously, and employ the Metamath eimm.exe utility to transfers proofs between the two proof assistants.)

For documentation, tutorial, etc., plus the full source code and .jar (java executables), download:

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

and

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

See also (new!): mmj2ProofAssistantQuickTips

Inspirational Quote

     "We have put ourselves to work for the sake
     of an idea, seeking by magnificent exertions
     to arrive at the incredible." ~ José Ortega y Gasset 
     -- http://www.des.emory.edu/mfp/impossibleG.html

Feedback

MMJ2 Laboratories, Inc. is interested in hearing from you about your happy or unhappy experiences with mmj2.

Please use the dedicated page for mmj2 Feedback/Questions: mmj2Feedback

Here is a dedicated page for feedback about the mmj2 Proof Assistant GUI: mmj2ProofAssistantFeedback

NOTE: To update the wiki your "username" must be "whitelisted". Send an email to the wikilord if you are not already a user – and, if you don't care to do that, I authorize you to post as "ocat" for the purposes of mmj2 feedback and problem reports, etc. (Just put some initials on your edits so I know who is doing what…)

ALSO, you may get the "Cannot acquire main lock" error message when attempting to post to the wiki. In this case, hit the Back button on your browser, open a new window and go to RecentChanges? then click on Administration, then Unlock Wiki. Wait, and then return to your original post and click on "submit" again.

--ocat 2007-10-15

Index of mmj2* pages

(This is wiki everything regardless of any "enduring merit". The mmj2 "doc" directory in the mmj2.zip download contains the most valuable information – whereas these pages contain tenative drafts and discussions, among other things, such as errors and possibly even misinformation, depending…)

antecedents

PrecomputationOfLogHypUnifiers

MaximallyCompressedMetamathDatabases

MergeSortedArrayLists

MetamathForProgrammers

mmj2-01-Oct-2007ReleaseEnhancements

mmj2ASCIITypesetting

mmj2BetaRelease01Sep2007Feedback

mmj2Feedback

mmj2FeedbackV20061101

mmj2FeedbackV20070716

mmj2Feedback20080113