Since I've been working with the Z notation, I have been looking for a suitable theorem proving program. On my quest for tool support, I have stumbled across Z/Eves.
Apparently it's pretty good, but it suffers from several problems:
- It's outdated (so uses Python 2.3).
- The source is closed.
- The original developer abandoned it.
Compile Python 2.3
At least the first of these problems are not insurmountable, although it involved a little bit of patience. My machine runs Ubuntu 8.10, which does not have any Python 2.3 support, otherwise it would be a simple case of
sudo aptitude install python2.3
Instead, I had to download the original source from here, and compile it myself. However, there's a bug that prevents this from working well, and so compiler flags are needed at the
Here's what I needed to do to get it up and running:
cd opt wget http://www.python.org/ftp/python/2.3.7/Python-2.3.7.tar.bz2 tar -xvjf Python-2.3.7.tar.bz2 cd Python-2.3.7 ./configure BASECFLAGS=-U_FORTIFY_SOURCE make
That's not all though, Z/Eves requires a little tweaking once it's been installed.
wget http://agamenon.uniandes.edu.co/~rcardoso/Cursos/MESw/Material/ZEVES/z-eves-2.3.tgz tar -xvzf z-eves-2.3.tgz
Now you need to modify the
z-eves-2.3/system/system/z-eves-gui.sh so that it looks like this:
zevesdir=~/opt/z-eves-2.3 zguidir=$zevesdir/gui-2.3 python=~/opt/Python-2.3.7/python zfontsdir=$zevesdir/zedfont lispdir=$zevesdir/system zsysdir=$zevesdir/system zlibdir=$zevesdir/library/ zeves=$zsysdir/z-eves-pc-linux-cmucl.core xset +fp $zfontsdir export LC_ALL=C export ZEVESCMD="$lispdir/lisp -core $zeves -- -libs $zlibdir" exec $python $zguidir/toplevel.pyc "$@"
It's important that you set a new
zfontsdir, and add the
xset line, since that will enable Z/Eves to display everything correctly.
For good measure I changed the
z-eves-2.3/system/system/z-eves.sh file to reflect a new
zevesdir too. Oh, notice that the original file uses
gui-2.2, rather than
gui-2.3. I don't know if this is because the 2.3 release isn't stable, but in either case, it seems that gui-2.2 doesn't work even with python2.3 (I expect it needs an even older version).
With all that done, I was able to run Z/Eves without any silly magic numbers getting in the way.