Next mmj2 Release: Step Prover

mmj2StepProver – ETA unknown, hoping for no later than 1-Apr-2009.

StepProverDoc.zip – documentation and untested source code for Step Prover (README.txt inside explains).

New version of mmj2 uploaded: 1-Aug-2008!

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

= 1,534,041 bytes (don't neglect to check the http://us2.metamath.org:8888/ocat/mmj2/mmj2.md5 ).

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

One way of looking at the release is that the main feature of interest to GUI users is the Theorem Loader, and the primary benefit of Theorem Loader is that it provides the effect of updating a Metamath .mm file with your mmj2 Proof Worksheets developed using the GUI. It also provides a "sandboxing" capability to automatically load the contents of your "MMT Folder" at start-up, so your sandbox is persistent across GUI sessions. The new "mmj2 Service" feature is also notable as it enables external code to interface with a running mmj2 instance.

Hope you digg it!

--ocat 21-Aug-2008

— 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