Z/Eves

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:

Unknown said...

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

Anonymous said...

thanks for instructions

Post a Comment