The policy here at MMJ2 Research Labs, LTD. is to catapult installation files over the castle walls, old school style. We love to hear the agonized shrieks and outraged complaints of our customers :) …So…
Feel free to complain about the Proof Assistant here!!!
Complaints about other aspects of mmj2 – general grievances -- should go here: mmj2Feedback
Previous Version of Feedback: mmj2ProofAssistantFeedbackV20060129
Welcome!
Here is a tutorial: mmj2ProofAssistantTutorial
And this has more helpful information, including a "quick howto", a detailed reference for the Proof Assistant GUI and information about the powerful new Derive feature:
http://planetmath.cc.vt.edu/~mmj2/
For someone new to Metamath proving techniques, a good start is to save a copy of this page showing the first 100 proofs in set.mm and then work through proving them, one by one:
http://us.metamath.org/mpeuni/mmtheorems.html
If you do not have unicode Math fonts you should go get them, but as a workaround use the GIF directories at Metamath, like this:
http://us.metamath.org/mpegif/mmtheorems.html
The 100th theorem in set.mm is pm2.521, so in your mmj2 RunParm file add this line right before the "LoadFile" RunParm line:
LoadEndpointStmtLabel,pm2.521
That will reduce the GUI time by a 10(?) by not loading 6000+ theorems, only the first 100.
1. The Proof Assistant has Derive, Renumber and Decompress, as requested! Derive, especially, is very powerful. Renumber was a quick fix, but helpful. Decompress speeds up the LoadFile operation by 50%, so that is very nice!
1.
You say to download the "JDK 1.5 compiler (Java Development Kit)" from http://java.sun.com/j2se/1.5.0/download.jsp. There are several downloads on that page that mention "JDK" and none mention anything about a "1.5 compiler". I selected "JDK 5.0 Update 6". Perhaps it would be good to make this explicit.
2.
When you say "Windows Command Prompt", you mean Start -> Run -> cmd, _not_ Start -> Run -> command. Maybe everyone "knows" this, but I rarely use it and keep mixing them up as I try to unremember my Windows 95 days.
I should say Windows Command Prompt Window, which is the modern analogue of the old DOS Window under Windows 3.1 etc. What I do is Start/Programs/Accessories and then right mouse button click "Command Prompt" and select "Create Shortcut" to put the Command Prompt Window icon on the desktop.
3.
When I ran C:\mmj2\compile\windows\CompMMJ.bat I got: C:\tmp>C:\mmj2\compile\windows\CompMMJ.bat ... C:\mmj2>javac @compile\windows\javacTCompilePaths.txt @compile\mmj\mmio\mmioClasses.txt 'javac' is not recognized as an internal or external command, operable program or batch file. … C:\mmj2>ECHO "*** CompMMJ?.bat ERROR ENCOUNTERED!" "*** CompMMJ?.bat ERROR ENCOUNTERED!" …
I had to do this: Start -> Settings -> Control Panel -> System -> Advanced -> Environmental Variables -> edit Path to append ";C:\Program Files\Java\jdk1.5.0_06\bin" and restart the Windows Command Prompt. (Later - I now see you mention this at the bottom of the page, but it should probably be part of the in-line instructions. Also, the path is obsolete in the bottom-of-page instructions. I wonder why Sun doesn't add to the Path in its Java installation?)
So noted. Thanks!
4.
You might mention C:\mmj2\test\windows\!BatchMMJ2Sample001.bat is the one for set.mm (or rather expset.mm). Or perhaps a more obvious name? The others seem to be test cases that probably wouldn't be of general interest.
C:\mmj2\test\windows\RunPAGUI.bat is the sample to kick off the GUI Proof Assistant. What I am doing is setting up a separate directory/folder elsewhere that is customized for my proof studies. Like c:\myproofs and then copy "RunPAGUI.bat" to there, along with its RunParm file, "RunParmFileRunPAGUI.txt" (update the "LoadFile" and "ProofAsstProofFolder" RunParm commands to point to the correct input files.
Then go into the Command Window and execute
cd: c:\myproofs runpagui
1. The proof text area is always in "Insert Mode", and the insert key doesn't toggle between replace and insert.
2. There is no Undo/Redo feature.
--> Added in Nov-1 Release. Note that after Unification Undo must be pressed TWICE -- the GUI creates two undoable actions when resending the page: update the text and position the cursor. The code to combine two undoable actions into one is a little tricky and I am not in the mood to attempt at this time. The bad part is that after the first Undo what is presented is a blank text area, but the second Undo restores the text in correct status.
3. Add code to the very beginning of BatchMMJ2 to verify that the Java runtime environment is compatible with the compiled code. This would be useful if/when compiled code is distributed.
--> Added in Nov-1 Release. Looking for version 1.5 or higher. Not sure how well this works in non-Sun runtime environments, but given the fact that Java Swing would be almost impossible to reverse engineer in a clean room, the open source community will need to wait just a bit more for Java to be released as open source...and then things will be beautiful...As is, we know that the Macintosh/Apple Java does not support mmj2's needs, but that mmj2 is runnable on Linux and Windows (using Sun's JRE environment.)
4. It does not output proofs in Metamath compressed format.
--> This is not impossible, but it is computationally intensive. Given that Metamath.exe now has an import/export facility for mmj2 Proof Worksheets, the priority of this item is lower than low. The reason why it might be done is that there are interesting algorithms for checking for repeated subproofs and this is an active area of research. My idea is to create a hash key for each node of a proof tree and then check a hash table to see if the sub-proof already exists for the proof.
5. Formulas are displayed as long strings that are hard to read. For example, Step 10 of theorem cdaassen comes out as
12::eqeng |- ( ( ( ( A X. { (/) } ) u. ( B X. { 1o } ) ) X. { (/) } ) e. V -> ( ( ( ( A X. { (/) } ) u. ( B X. { 1o } ) ) X. { (/) } ) = ( ( ( A X. { (/) } ) X. { (/) } ) u. ( ( B X. { 1o } ) X. { (/) } ) ) -> ( ( ( A X. { (/) } ) u. ( B X. { 1o } ) ) X. { (/) } ) ~~ ( ( ( A X. { (/) } ) X. { (/) } ) u. ( ( B X. { 1o } ) X. { (/) } ) ) ) )
--> The new TMFF -- Text Mode Formula Formatting enhancement is a glorious achievement :) Will be available in the Nov-1 release!
Would it be possible/useful to output using the Unicode typesetting specified in the input .mm file, along with new typesetting specifications at the syntax axiom level (the formula parse trees would be input to the formatter)? The user would continue to input the ASCII equivalents (as shown above), which would be converted to Unicode for re-output. A switch to a variable width font might help too. --ocat 3-Apr-2006
6. (Suggestion) On the mmj2 doc page, you have:
2. As of April 1, 2005, mmj2 contains processing to perform validation of www.Metamath.org ".mm" files (also called Metamath databases), Proof Verification, extremely basic printing of the contents of a .mm file, grammatical parsing, and proving with a GUI Proof Assistant.
- It does not do anything with Metamath Comment Statements - It does not produce beautiful html pages like metamath.exe. - It does not update an existing .mm file.
Regarding the last point, you may want to mention the worksheet export/import facility eimm that does allow (indirectly) updating a .mm file, as well as allowing you to go back and forth between the mmj2 and metamath PAs, giving you access to the best features of each. I also wonder if anyone other than myself is actually exploiting the power of eimm, since I've heard no feedback. Or maybe it's just because there are no bugs. :) But more likely it's because almost no one is aware of it, so it might be useful to mention it in your doc page. --norm 14 Aug 2006
with a proof,
1. The cursor positioning code does not always put the cursor exactly at the first error on the screen.
--> Big improvements coming in Nov-1 release!!!
2. A very minor nuisance (put it near the bottom of your to-do list):
If you Exit/Quit, the getYesNoCancelAnswer() box comes up. In most programs, if you click on the upper right X in such a box, the action is the same as if you clicked on Cancel. In mmj2, the action is the same as if you clicked No.
If, instead of Exit/Quit, you click on the upper right X in the main screen, the getYesNoAnswer() box comes up. First, there is no Cancel option. (Most programs have one under this condition.) But again, if you click the upper X of the getYesNoAnswer() box, the action is No rather than Cancel, so once you get to that box there's no way to cancel.
--> Will be fixed in Nov-1 release. 'x' button press to close window invokes yes/no/cancel dialog if changes need saving, and the yes/no/cancel dialog treats 'x' button press (close of the dialog window) as a CANCEL.
Hi frl, Glad to see you are back on the Lambda Calculus My brain is tired so I cannot begin to comprehend what you wrote, but it is nice to hear from you again! The Renumber feature in mmj2 is now available. I think you will also appreciate the Derive feature. --ocat 4-Apr-2006
Hi ocat, I'm happy you released a new version. I shall try it as soon as possible (i.e. as soon as I remember to take a usb key and to go to a place where I can download it ). – frl 4-Apr-2006
That's ok. I've tried it and everything works perfectly. Thank you for the "Renumber" feature. Proving is much easier this way. I have not yet used the "Derive" feature. It is less important for me since I often make my proofs using cutting and pasting but I shall try it as well. What are your plans for the future ? – frl 5-Apr-2006
I've tried the "Derive" feature. It's nice as well. If you need end-user requirements, don't hesitate: I have some. – frl 6-Apr-2006
Ok I'm working on a proof. After some time. I get something like this:
h1:: # G |- fubar 210:: # G |- farbu 21:210: # G |- barbar 20:1,210: # G |- barfu 2:20,21: # G |- bar qed:1,2: # G |- fu
Now I use the renumber derive feature, I get:
h1:: # G |- fubar 2::e # G |- farbu 3:2:d # G |- barbar 4:1,2:c # G |- barfu 5:4,3:b # G |- bar qed:1,5:a # G |- fu
Much better. But I'd like that the #s are in a row (new possible feature #1).
h1:: # G |- fubar 2::e # G |- farbu 3:2:d # G |- barbar 4:1,2:c # G |- barfu 5:4,3:b # G |- bar qed:1,5:a # G |- fu
This way it's pretty esthetical. But the tree-like aspect of the proof is not respected. 2 and h1 should be duplicated. And the order of the lines should be reorganized. ( new feature #2)
h1:: # G |- fubar 2::e # G |- farbu 3:2:d # G |- barbar h1:: # G |- fubar 4::e # G |- farbu 5:1,4:c # G |- barfu 6:5,3:b # G |- bar qed:1,6:a # G |- fu
And even we could increment the number of spaces in the most metamath-like manner ( new feature #3).
h1:: # G |- fubar 2::e # G |- farbu 3:2:d # G |- barbar h1:: # G |- fubar 4::e # G |- farbu 5:1,4:c # G |- barfu 6:5,3:b # G |- bar qed:1,6:a # G |- fu
This time a marvellous feeling of joy fills up the amateur of logic I think. frl 7-04-2006
I open mmj2 with let's say nat.mm. But when the proof is completed I need to copy it and to paste it into another editor. I never work with Windows, so I don't have good editors under it. So I would prefer to be able to load nat.mm in another tab in mmj2, and perhaps set.mm as well. Obviously I would need to be able to search for strings in these two tabs. frl 7-Apr-2006
I'm in an internet café. I have some time to spend. I want to make a proof. I connect myself to a very good web site (let's call it www.metamath-inline.org ). An interface appears on the screen that really looks like mmj2. I can ask to work with a database available on the server. For example set.mm (or nat.mm). I click on "new". I enter a proof. While working I can browse proofs in another good site (www.metamath.org). One hour later the proof is not finished. I save it in a private area on the server. Later I resume. This time I load set.mm and my new partial proof. --frl 8-Apr-2006
Suppose I want to revise an existing proof ... How do I bring the existing proof into the GUI window? If I select "New" (I don't see any other option for this) and specify an existing and proved theorem e.g. a1i, it pulls in the hypothesis and conclusion correctly, but the proof is gone. Perhaps you have to reenter all the steps by hand, but somehow I don't think you did this ... Also, the "default" syl _is_ brought in with its complete proof, so I assume there must be a way to do this.
Right now the primary way to do this is with the "ProofAsstExportToFile" RunParm command, which puts an existing proof into a file. Here is an example:
*********************************************************** * NOTE: An asterisk or blank in column 1 signifies Comment. * The following commands are indented for the Asteroid, * so shift following lines LEFT by 4 columns before use! *********************************************************** *================================================== * CommentLine: Example Running ProofAsstGUI *================================================== MaxStatementPrintCount,9999 MaxErrorMessages,15000 MaxInfoMessages,1000 LoadEndpointStmtNbr,999999999 LoadEndpointStmtLabel,ZZZZZ.999999999 LoadFile,c:\metamath\set.mm VerifyProof,* Parse,* * VerifyParse,* *PrintSyntaxDetails *PrintStatementDetails,dummylink RecheckProofAsstUsingProofVerifier,yes ProofAsstFontSize,12 ProofAsstFormulaLeftCol,20 ProofAsstFormulaRightCol,100 ProofAsstRPNProofLeftCol,5 ProofAsstRPNProofRightCol,79 ProofAsstUnifySearchExclude,biigb,xxxid,dummylink ProofAsstMaxUnifyAlternates,10 ProofAsstDummyVarPrefix,$ ProofAsstProofFolder,c:\mystuff\mmj2\myproofs\oldfix ProofAsstExportToFile,unxpdom2,unxpdom2.mmp,new,unified,NotRandomized,Print ProofAsstExportToFile,sucxpdom,sucxpdom.mmp,new,unified,NotRandomized,Print ProofAsstExportToFile,uncdadom,uncdadom.mmp,new,unified,NotRandomized,Print ProofAsstExportToFile,cdaen,cdaen.mmp,new,unified,NotRandomized,Print ProofAsstExportToFile,cda1en,cda1en.mmp,new,unified,NotRandomized,Print ProofAsstExportToFile,cdacomen,cdacomen.mmp,new,unified,NotRandomized,Print ProofAsstExportToFile,cdaassen,cdaassen.mmp,new,unified,NotRandomized,Print ProofAsstExportToFile,xpcdaen,xpcdaen.mmp,new,unified,NotRandomized,Print ProofAsstExportToFile,mapcdaen,mapcdaen.mmp,new,unified,NotRandomized,Print ProofAsstExportToFile,cdadom1,cdadom1.mmp,new,unified,NotRandomized,Print * ProofAsstBatchTest,xpmapenlem3,xpmapenlem3V1.mmp,unified,NotRandomized,Print RunProofAsstGUI
The output files are using a ".mmp" suffix, but ".txt" is good too. Specify "new" if the file does not exist, or "update" if it does.
Use "File/Open" option in GUI to open .mmp file created by ProofAsstExportToFile RunParm.
The C:\mmj2\test\windows\RunVolumeTest2.bat file distributed with mmj2 shows how to run every proof in set.mm through the Proof Assistant in batch mode (takes a few minutes to run).
Perhaps a GUI option to display an existing proof will be added some day…
--ocat 12-Apr-2006
Suppose you're working on a proof in the Metamath program's Proof Assistant, then you decide you'd like to switch over to mmj2's PA GUI to finish it.
I wrote a proof-of-concept program, "eimm" (pronounced "aim"), that exports a proof-in-progress (that can have unknown steps) from the Metamath program's Proof Assistant. It can be downloaded here: eimm
To run it, you put the files eimm.exe (or compiled eimm.c on Linux) and eimm.cmd somewhere in your directory path, such as the current directory you are in. Inside the Metamath proof assistant, type "submit eimm.cmd".
For example, suppose we 'prove equid2' and 'delete step 33'. That simulates an incomplete proof in progress. Then we type
MM-PA> submit eimmexp.cmd Taking command lines from file "eimmexp.cmd"... ... The output file will be called "equid2.mmp". MM-PA> [End of command file "eimmexp.cmd".]
which will produce the file "equid2.mmp":
$( <MM> <PROOF_ASST> THEOREM=equid2 LOC_AFTER=?
1::a9e |- E. y y = x 2::ax-17 |- ( x = x -> A. y x = x ) 3:: |- ( y = x -> ( y = x -> x = x ) ) 4:3:pm2.43i |- ( y = x -> x = x ) 5:2,4:19.23ai |- ( E. y y = x -> x = x ) qed:1,5:ax-mp |- x = x
$)
When Open'ed with the mmj2 GUI PA, "StartUnification" will automatically figure out the missing step in this example and produce the completed proof.
The created file "equid2.mmp" will not overwrite previous versions; instead they will be renamed to "equid2.mmp~1", "equid2.mmp~2", etc.
The eimm C program can also be run stand-alone; see "eimm --help". Eventually it might be possible to add a native export command to the metamath program after some experience is gained with eimm. However, it doesn't seem overly inconvenient to run the way it is, for the time being.
--norm 13-Apr-2006
Suppose you're working on a proof in the mmj2 GUI Proof Assistant, then you wax nostalgic and decide you'd like to switch over to the Metamath program's old-fashioned CLI for a while (see 5a above for going back to the GUI; also note that eimm.cmd was changed to eimmexp.cmd there).
The eimm program has been enhanced with an import option. The new version is here: eimm. Important: The Metamath program must be upgraded to version 0.07.16 or greater in order to use the import feature of eimm.
To run it, you put the files eimm.exe (or compiled eimm.c on Linux) and eimmimp.cmd somewhere in your directory path, such as the current directory you are in. Inside the Metamath proof assistant, type "submit eimmimp.cmd", followed by "submit tmp.cmd".
For example, suppose we have a proof worksheet for equid2, called equid2.mmp. To import this worksheet, we type
MM> prove equid2 MM-PA> submit eimmimp.cmd MM-PA> submit tmp.cmd
which will delete any existing proof of equid2 and build a new one from the mmj2 worksheet equid2.mmp. (The file tmp.cmd is generated by elimmimp.cmd, but it has to be run separately because Metamath doesn't allow 'submit's inside of a command file.)
Most incomplete proof worksheets should be acceptable, including ones with "incomplete but valid" steps that ocat described above. Orphaned subproofs (which metamath's MM-PA doesn't allow natively) are patched into the main proof by using the "dummylink" theorem, so that their information will not lost; after the proof is complete, MM-PA's 'minimize' command will purge all dummylinks.
--norm 17-Apr-2006
A newer, slightly cleaned up version (0.03) of eimm is available today. --norm 18-Apr-2006.
Some notes:
I chose to make eimm an external program for easier debugging. It talks to metamath.exe via command files, so you see a lot of stuff scroll by on the screen, which is annoying but at least it helps debugging. Once the algorithm is perfected, I could eventually add native 'export' and 'import' commands to metamath.exe, so all the stuff could happen silently. Oh, the bloat inside of metamath.exe…
By the way, the change in Metamath 0.07.16 added relative 'assign' and 'let step' step numbers that extend the concept of the existing 'assign last' that assigns the last unknown step, so that 'assign -1 syl' will assign syl to the penultimate unknown step, 'assign -2 syl' to the antepenultimate, etc. 'help assign' and 'help let' describe these. These made it possible for eimm to skip unknown proof worksheet steps without knowing the step numbers, making eimm much easier to write, but I can also see them as handy for human users such as myself. --norm 19-Apr-2006
I think $d statements should be treated as any other hypothesis. In particular they should appear in the window and the Unification feature should not try to unify if the proviso is not mentionned on the page. – frl 16-Apr-2006
Oh, please. Thou strainest at the gnat but swalloweth the camel :)
mmj2's ProofAssistant goes to eXtreme lengths in support of $d restrictions.
First of all, it employs $d restrictions contained in the input .mm file – but it does not display the existing $d's on the screen because of the problem of combinatorial explosion, which results in bazillions of $d pairs for many theorems, and would fill the screen; the user can simply look at the source file and see the pre-explosion information. (In theory the internal set of distinct variable pairs could be re-converted back to a minimal set of $d statements, for display purposes – and then un-re-converted at proof check time.)
Second, the mmj2 Proof Assistant allows extra $d's to be added, either to an existing proof or to a new proof not in the input .mm file.
Third, in the event that the computed Ref (Assrt label) results in a $d error, the Unification search process provisionally accepts the Ref, generates an error message and then continues the search through the assertion database (list), looking for a Ref which meets the unification criteria but does not violate $d restrictions. If a better fit is found it is accepted, and if not, an error message listing the alternative Refs (that also have $d errors) is displayed.
Finally, in the event that the mmj2 Proof Assistant's method of generating a unifying set of substitutions that are consistent across the set of proof assertions has a theoretical flaw, a RunParm option is provided to always double-check the Proof Assistant's generated proof using the Metamath Proof Verification algorithm (and I recommend always using this RunParm unless/until the unification algorithm is proven to be mathematically perfect – which I cannot/have not done.)
So for any given Derivation step the user has two choices: chooose another Ref or add $d restrictions to the proof. And, I think Norm has a utility that will generate $d's ex post facto.
--ocat 16-Apr-2006
frl dons his VR gear and logs on to an OpenCroquet server to view the latest art exhibit:
http://www.wetmachine.com/itf/item/477
Inside he meets his friends ocat and norm who are debating the latest quirks of Metamath. All three decide to jump to the Metamath Metaverse which is running on a Croquet server in a different country, but the jump is instantaneous. They appear at the entrance to the Hall of Logic.
Just inside the Hall of Logic are exhibits that look like abstract art but are actually the latest quantum-modal logic axiom scheme which is represented in 3D systems of equations involving multi-colored shapes, symphonies of music and "smello-vision" :)
They hop on a tram because the Metamath Metaverse is too big to traverse on foot, because of the 1 billion Mathelogicians laboring inside the Truth Mines (not counting the AI's working the knowledge faces on a contract basis.) Thanks to full 3D VR typesetting of Metamath equations, and particularly the VR interface, Math and Logics have become the latest planetary fad -- a fad that has persisted for centuries but shows no signs of dying out. (The ocat avatar is a simulation -- ocat's 9th life was lost during the Biq Quake of 2006, but norm and frl are "real", geezers who have been rejuved many times…for the year is 3006…)
blah-blah.
--ocat 22-Apr-2006
The adventurous mmj2 user fires up the mmj2 process using the new RunXhtmlProofAssistant run parm and a webpage interface appears with MathML rendered formulas. He double-clicks on a formula and a clone of the ASCIIMathML program is invoked for editing of the Metamath symbols that are cunningly stored in the ALT Text area. After modifying a formula the user clicks the Unify button and the unification request is sent to a server running on the user's PC – the server calls the mmj2 ProofUnifier.java function to handle the request and receives back the updated Xhtml page (the .mmp text version of the proof text area is also stored on the user's hard drive to maintain compatibility with Metamath's eimm.exe Export/Import utility.)
(Note: a new mmj2 utility program creates a clone of ASCIIMathML based on the contents of an input .mm file.)
Later, the user visits metamath.org/mathml/* to view the MathML-rendered webpages for set.mm.
Update: A quick review indicates that - ASCIIMathML provides the technological approach we need, but not as-is. Output MathML codings will need to be based on Metamath syntax axioms, not just the Unicode character codings desired. Therefore, an input formula will need to be parsed by mmj2 before handoff to the ASCIIMathML-variant's MathML encoder. - A standalone webserver will be needed that can read the HTML page containing the proof and invoke mmj2's Proof Assistant routines. It appears that something like NanoHTTPD would do the job – or, if necessary, Jetty, for the full-blown server.
This enhancement would be the single-user, single-threaded version of the mmj2 Proof Assistant. Ideally, the user would be able to toggle between the Java GUI version and the HTML version of a proof. Regardless of that though, the output proof text file – the .mmp – must be unchanged so as to maintain compatibility with Metamath's new "eimm" feature (export/import of mmj2 proofs).
Note: it may be that an enhancement to the formatting of the mmj2 GUI's formulas should be done at the exact same time – this would continue to display formulas in ASCII as is done today, but would insert line breaks intelligently using the syntax axiom formatting specifications that will be needed for the HTML pages.
Any insights on the nature of the webpage design would be appreciated. It might be that something very similar to the Metamath Proof Explorer webpages could be used (it would be wild to have the program capable of actually reading those pages!) Something more graphical might be considered, but I have no expertise in these matters and unless I get some help from a smart person I'll end up doing it the simplest way possible that gets the job done.
--ocat 25-Apr-2006
I think that three things are needed. In a window, an editor (in the mmj2 style), in another window an access to the database (in the metamath proof explorer style). I think it is also needed to perform regular expression searching in the database. I don't know how Norm or you look for theorems in set.mm but for my own part, I often using M-x string-search in emacs using inputs like ( A. x ph → A. y ph ) or data keywords like 'axiom of choice' and so on. Such a simple device should be included to the whole server structure.
You had suggested that we could give a graphical appearance to the formula using TeX? as a server. In my opinion it is the simplest way. We can imagine that each line is formatted using TeX? and that pictures are combined together then to form an html page. – frl 27-Apr-2006
Hi frl, my primary motivation right at this moment is to typeset/format formulas in mmj2, particularly in Proof Assistant, which is the most interesting and appealing portion of mmj2 (perhaps the only interesting and appealing part of mmj2 from the perspective of most users :)
What the means in practical terms is that I want to focus like a laserbeam on this one thing and make it happen in my lifetime. Then, when this major piece of the puzzle is in place, there may be time to redo everything properly with a multi-threaded, multi-user server architecture with tight integration of all features.
For now I am hoping that you can continue to use emacs to do searching, and metamath.exe to do what it specializes in, and so on.
If we look here, set.mm definitions, we see that just Unicode and basic html coloring, etc. can produce a visual improvement over the ASCII encodings (which, as I understand them, were originally based on LaTex?).
I am thinking that MathML is a good tool for adding typesetting and formatting to a Proof Assistant front-end because MathML is tightly integrated into many web browsers, along with SVG, which may also be of use (somehow.) I am not opposed to using LaTex or Tex or whatever, in theory, but…
I do not believe that a user would find either the raw MathML or Tex encodings useful for editing, not for long, complicated formulas anyway; so my question is, what will produce the best results for viewing Metamath formulas?
Here are a few related items I came up with:
1. A typesetting preference/parameter file should be separate from set.mm (or ql.mm, etc.) so that a user may choose his/her own viewing experience.
2. It may be that visual perceptions of Metamath formulas will be enhanced if nested parentheses (and other bracketing constants) have varying sizes. So, the outermost parentheses would be largest and the innermost would be the smallest. It may be that using bold or colors would also be helpful. Either way, this concept would be controlled by user-settable preference/parameters.
3. The number one problem in typesetting Metamath formulas is intelligent linebreaking. This is especially grievous for the really long formulas(!)
4. The number two problem in typesetting Metamath formulas is ???
--ocat 27-Apr-2006
A source of confusion about the mmj2 Proof Assistant is that a New Proof's scope is always at the global level, regardless of its position as specified by LOC_AFTER on the Proof Worksheet (if LOC_AFTER is not specified the position of the new proof for validation purposes is at the end of the input .mm database.) For example, assume that the input .mm file has these $e statements which serve at "placeholders" for future work:
${ $( new scope begin, level is global + 1 $) xyz.1 $e |- blah blah $. abc.1 $e |- blahblah blah blah $. $}
Now, if the mmj2 Proof Assistant user starts a new proof for theorem xyz – which does not exist in the input .mm database – a "duplicate label" error message results.
h1::xyz.1 |- blah-blah 2:1 |- ergo blah blah qed:2 |- daDa!
In fact, if the user had not explicitly entered "xyz.1" as the Ref for Step 1, the program would have generated it – and then flagged the error. That is because the default label for hypothesis step Refs is label.1, label.2, label.3, etc.
To eliminate the error simply change the Ref on Step 1 to "xyz.h1" or go back into the .mm file and add a "xyz $p" statement in scope of the "xyz.1 $e" statement.
Note also that LOC_AFTER cannot – does not – insert a statement within a nested scope level in the input .mm statements. Once the scope is closed via a "$}" statement, that scope is closed to the world like matter beyond the event horizon of a black hole.
Another topic of interest is $d's. The Metamath.exe Proof Assistant does not validate distinct variable restrictions, and so may consider a proof valid even though it contains $d errors. However, when such a proof is exported via EIMM.exe to a Proof Worksheet and Unified via the mmj2 Proof Assistant, the user may be shocked when he/she receives 100 error messages about violations of $d restrictions.
Note also that when mmj2 directly imports a Metamath RPN-format proof, if the proof is incomplete or invalid, mmj2 will report an error and, depending on context, produce nothing or a skeletal proof. This is a result of mmj2's very primitive algorithm for converting an RPN format proof to the Proof Worksheet format.
Fortunately for everyone, mmj2 and Metamath.exe can work well as a team. You can run mmj2 in one command window and Metamath.exe in another. The fact that mmj2 does not update Metamath .mm databases is not a problem because Metamath's EIMM.exe can Import a proof that is in mmj2 Proof Worksheet format (even incomplete mmj2 proofs!)
mmj2 and Metamath.exe's "teamwork" is one reason why mmj2 makes no attempt to replicate every feature of Metamath.exe – it would be redundant because metamath.exe works great for these tasks that mmj2 does not attempt.
--ocat Oct-8-2006.