Andrius Velykis Andrius Velykis

Installing Z/EVES on Mac OS X

Z/EVES for Eclipse

Z/EVES is an interactive theorem prover for Z notation. It can be used to develop Z specifications and reason about them. It has a number of attractive features, such as an easier learning curve (in comparison to related theorem provers, e.g. Isabelle), powerful proof tactics, and the ability to do proofs in Z notation.

Unfortunately, it is no longer being developed. Neither is it open sourced (as of the time of writing), so we have to make do with what we have: the last version (2.4.1 apparently) was released in 2005 for Windows, Linux and Solaris platforms. There is no Z/EVES runtime for Mac OS X, however, which is problematic knowing that Macs are not rare in academia..

Fortunately, I have managed to get the Windows version of Z/EVES running on Mac OS X using Wine. I could install Z/EVES on my OS X Lion to run both as command line (to integrate with CZT Eclipse!—see screenshot) as well as using its Python GUI. The (more) detailed instructions follow.

To install Z/EVES, you need to install Wine on your Mac, then install Z/EVES for Windows using Wine (as well as Python 2.3 if you want to use the original GUI), and finally configure it to be launched conveniently. For the best experience, run Z/EVES within Eclipse IDE as part of Community Z Tools.

Install Wine

Wine is a compatibility layer that allows running some Windows programs on Linux, Mac OS X and other operating systems. It is different from BootCamp or virtualization options, in a way that the program actually runs on Mac OS X, with Wine translating Windows API calls into POSIX calls.

I will not give detailed instructions how to install Wine: an excellent and detailed tutorial is available here. Refer to it to get Wine on your Mac as well as on how to install Windows applications. To summarise, you need the following:

  1. Install Xcode with Command Line Tools.

  2. Install XQuartz—X11 server for Mac OS X.

  3. Install MacPorts.

    Install Homebrew.

  4. Install Wine using MacPorts (package wine). Note that if you encounter problems running Z/EVES, you could try installing wine-devel, which is a more “cutting-edge” version of Wine.

    Install Wine using Homebrew: brew install wine.

Update: MacPorts is no longer the preferred way of installing Wine—use Homebrew instead. Also, Wine ≥ 1.6 no longer needs X11 on Mac OS X.

Install Z/EVES

To install Z/EVES, open the terminal at the location of the Z/EVES Windows installer. Then you can launch the installer using Wine, e.g.

wine z-eves-install-2.3.exe

It will launch the X11 server and with it the Z/EVES installer (appearing in the Classic Windows style). You can install Z/EVES into C:/Program Files as usual on Windows—this will place the program under ~/.wine/drive_c/Program Files/ in your home folder.

Z/EVES does not require to be in Program Files, so alternatively you can select the Z:/ drive in the installer, and install it, say, to Applications so that it is easily accessible from your desktop: e.g. Z:\Applications\zeves23. Now Z/EVES is available under /Applications/zeves23.

Run Z/EVES

Now you should be able to run the command-line version of Z/EVES using wine command:

wine /Applications/zeves23/system/z-eves-pc-windows-lispworks.exe
Z/EVES cmd

Run Z/EVES with Python GUI

Z/EVES ships with an additional Python user interface to drive the theorem prover. Since the last version of Z/EVES was released in 2005, and Python are not too keen on backwards compatibility that much back, you need to get an older version of Python runtime. For example, Z/EVES 2.3 requires Python 2.3.x. Download a Windows installer for Python 2.3.5 from their website. Install Python using Wine just like you did for Z/EVES, e.g. to Z:\Applications\Python23.

Z/EVES was developed as a single-processor application and frequently crashes on multi-processor computers. Nowadays multicore processors are common, so to avoid the crashes, we need to make Z/EVES use only one processor. This is normally achieved using the Task Manager in Windows, via Set Affinity command. For Wine, however, the command is not easily accessible.

To streamline this, I am using a utility called RunFirst, which does exactly the same thing. Download the executable, and place somewhere close to Z/EVES, e.g. in /Applications/RunFirst/RunFirst.exe.

Now I use a batch file (zeves-gui.bat) to launch Z/EVES GUI in Windows using RunFirst and Python, then call this .bat file from Mac OS X using a command-line script zeves-gui.sh:

  • zeves-gui.bat:

    ..\RunFirst\RunFirst.exe "..\Python23\pythonw.exe gui\toplevel.pyw --debug"
    
  • zeves-gui.sh:

    #!/bin/sh
    /opt/local/bin/wine cmd /C zeves-gui.bat
    

I put these files in the Z/EVES directory, so update the relative paths for your installation, if needed. I have attached these files below for your convenience:

Now when you launch Z/EVES using zeves-gui.sh, it will start the Python GUI. Note that you can also package this into a Mac App to have it clickable in the dock, as explained in this tutorial.

Z/EVES Python GUI

Run Z/EVES within Eclipse using CZT

To circumvent the limitations of the ageing Python GUI of Z/EVES, we have integrated Z/EVES with Community Z Tools (CZT) and Eclipse IDE. The integration will be part of the upcoming CZT 1.6 release, which we are preparing at the moment. You can get a preview with the ‘nightly’ builds available from this Eclipse update site:

http://czt.sourceforge.net/eclipse/updates/latest

Install the plug-ins using Eclipse Update Manager. When installed, launch Z/EVES as an external tool—just point to the Z/EVES command line executable (zeves-cmd.sh, available in the archive above) and indicate Z/EVES working directory.

The integration has everything the Python GUI has, and more, thanks to integration with CZT:

  • Develop Z specifications using Z LaTeX or Unicode syntax.
  • Document outline and navigation.
  • Section management (not available in the original Z/EVES).
  • Streamlined interaction with the prover, e.g. the commands are automatically undone up to a point where you edit the specification.
  • View proof goals anywhere in the document.
  • Integrated error reporting.
  • Theorem viewing.
  • Verification condition generation.
  • …and more!

More documentation will be available upon the official release of CZT. For now, the obligatory “screenshot, or it didn’t happen”:

Z/EVES for Eclipse
Z/EVES for Eclipse

Topics: Coding - Useful - CZT - howto - Z/EVES # Top


comments powered by Disqus