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.
Sigh.
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 ./configure
stage.
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
Install Z/Eves
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.
2 comments:
thank you very very much for this information , a few information in the web for Z-eves and specification in general
i have one question if you can answer me : how to generate document latex directly from Z-eves specification ??
thank you for all
thanks for instructions
Post a Comment