Here you can download the metamath integrated development environment
that I am working on. These instructions are repeated in the readme
file of the downloaded Python mmide zip file.
Note that this program will only run on a current Macintosh computer.
- Download the Python_mmide.zip
file.
- You need to unzip the mmide.zip file that you downloaded. It will
expand into a folder called "Python mmide".
- You need to download the PyGUI framework from the web site
located at:
http://www.cosc.canterbury.ac.nz/~greg/python_gui/
- Copy the folder GUI from the PyGUI folder into the folder "Python
mmide".
- Run the Python program mmide.py using your favorite method. You
need to
insure that pythonw is used, not python, since the program uses the
Cocoa graphical framework.
- Close the initial window named "set.mms"
- Using the program file menu, open the metamath database file
"miu.mms" located in the "Python mmide" folder.
- Using the program project menu, compile the program.
- If you wish, you can now save the compiled program using the
project
menu. The name of the compiled program will have "mmo" as its file
extension. The next time you run the mmide program, you can just load
the compiled program.
- Now type "theorem1" in the window's label field and hit the enter
key.
You can use the "Statement" and "Proof" menus to toggle what is
displayed.
- Of course, it is better to view the metamath database file
set.mm. You
need to download the metamath system from the web site located at:
http://us.metamath.org/index.html
Note that you have to convert the file set.mm from its compressed
format into its uncompressed format, naming it "set.mms". Be sure that
the "mm" extension is no longer present. Otherwise, the mmide program
will not recognize it as a valid database file when you try to open it.