Prover9-Mace4 v05
- This is a Graphical User Interface for
Prover9 and Mace4.
- It was constructed with Python and the WX widget library.
- The target platforms are Windows (2000 or later),
Mac OS X (10.3.9 or later), and Linux.
- To get started:
- Install the GUI (see the following sections).
- Start the GUI and see "File->Sample Inputs" and
"Help".
- See the Prover9/Mace4
Manual
and
Examples.
- The GUI contains Prover9 and Mace4, so there is no need to
also install the LADR system.
Windows
Download: Prover9-Mace4-v05-setup.exe
(about 5.2 MB)
- This will lead you through a standard Windows installation.
(You have to be an administrator.)
Known Windows Problems
- When both Prover9 and Mace4 are running, the GUI response is slow.
- Automatic syntax highlighting is annoying, so it is disabled
on startup.
- If you try to start the GUI and you see an error message that the
dll MSVCP71.DLL is missing, you can download it here:
MSVCP71.DLL, and then place it in the
directory "C:\Program Files\Prover9-Mace4".
Macintosh
Download:
Prover9-Mace4-v05B.zip (about 9.2 MB)
- If you put this on your Desktop and open (unzip) it,
the Prover9-Mace4 app should appear on your Desktop.
Known Mac Problems
- NOTE (March 14, 2008): There is a bug in the December 2007 version
(Prover9-Mace4-v05.zip), which caused changes in the parameters
(max_seconds, etc.) to not be sent to Prover9 or Mace4. Version v05B
contains a fix. This problem does not occur in the Linux or Windows
versions.
-
On an old iBook (G3 with 10.3.9), the text boxes that contain a lot
of output (>32K?) don't show scrollbars. All of the text really is
there, so it can be 'Save'd. This problem did not occur on the
Intel Macs (10.4, 10.5) we used for testing.
Linux
Download: p9m4-v05.tar.gz
(about 1.7 MB)
- This is not a self-contained package like the Windows and Mac
versions.
- You'll need Python 2.5 (or later) and Python-wxgtk2.6 (or later).
- In Ubuntu, you can install packages python2.5 and python-wxgtk2.6.
- Unpack p9m4-v05.tar.gz and run p9m4-v05/prover9-mace4.py.
- The included prover binaries (prover9, prooftrans, mace4, interpformat,
isofilter, isofilter2) are compiled for i386.
If you have different hardware, you can fetch
LADR-Dec-2007.tar.gz,
compile, and replace those 6 binaries in the directory p9m4-v04/bin.