These instructions assume you are running Linux.
On some Linux distributions (Ubuntu, Debian, Arch), Why3 is available though the package manager. However, on Ubuntu and Debian Stable, this is an older version, and on Debian Testing/Unstable, it is (at the time of writing) missing the graphical interface. Similarly, SMT solvers (such as CVC4, Z3, Alt-Ergo) might not be offered in a version compatible with Why3. Therefore I would recommended installing it manually.
There are two ways of doing this:
Using the prepared distribution. This contains Why3, a couple of useful provers, and it will probably work if your system is a reasonably recent Linux distribution.
Building it yourself, and installing recommended provers manually.
Using OPAM. This method has been reported to work well on MacOS.
If you find errors in this document, or something doesn't work for you, please let me know!
If you don't run Linux, or cannot get Why3 to run, see here
First, you will need to install the library GtkSourceView2. On Debian/Ubuntu, you can do this by:
$ sudo apt-get install libgtksourceview2.0
Then, download the distribution files for this course:
$ wget http://cs.ru.nl/~mschool/swan2019/why3-distro.tar.xz
This contains a file hierarchy that is suitable for installing on top of your existing /usr/local hierarchy:
$ sudo tar xvfJ why3-distro.tar.xz -C /usr/local
If you don't want to modify your system, you also install it wherever you want, but then you will need to add that location to your PATH:
$ tar xvfJ why3-distro.tar.xz -CDESTINATION_FOLDER
\( export PATH=\)PATH:DESTINATION_FOLDER/bin
After installing, why3 needs to know what system it is running on, and what provers are available to it:
$ why3 config --detect
And, if you are a vim user, you will probably want the syntax highlighting:
$ cp -r /usr/local/share/why3/vim ~/.vim
This is the more time consuming option. I am assuming that you are running a system similar to Debian Buster (the current Testing distribution). On Ubuntu, the steps should be similar. If you are running Arch Linux, you probably know what to do. Steps similar to those below might or might not work on.
Note that following these steps will put files in your /usr/local hierarchy.
Install the Ocaml compiler.
$ apt-get install ocaml ocaml-native-compilers
Download and unpack why3, and then enter the build directory. Take a look around, especially at INSTALL.md.
$ wget https://gforge.inria.fr/frs/download.php/file/37842/why3-1.1.1.tar.gz
$ tar xvfz why3-1.1.1.tar.gz
$ cd why3-1.1.1
Why3 has some dependencies needed to compile, so now is a good time as any to install these:
$ sudo apt-get install menhir libmenhir-ocaml-dev liblablgtk2-ocaml-dev liblablgtksourceview2-ocaml-dev
$ sudo apt-get install libzarith-ocaml-dev libzip-ocaml-dev libocamlgraph-ocaml-dev
(Optional) The Coq proof assistant might be useful to have. If you find yourself reaching for it (or you like using it), it is useful to have it installed before you build Why3. However, the course should be doable without it.
$ sudo apt-get install coq coqide
Now let's see if we can build why3!
$ ./configure
This should produce a meaningful summary of how Why3 will be installed, if not, you may be missing a dependency. If everything is okay, build it:
$ make
If again everyting went well, you are ready to install Why3.
$ sudo make install
For more information, consult the official manual.
We also need to install a few automatic provers before we can use Why3. Having multiple provers installed is recommended.
These provers are part of Debian, so we can just install them:
$ sudo apt-get install cvc4 z3
Currently, Alt-Ergo also has to be built manually. The Debian repository contains a version that is not supported by the latest version of Why3 (and has known defects). This routine is the same as for Why3, just a little less work:
Download and unpack the Alt-Ego sources
$ wget https://alt-ergo.ocamlpro.com/http/alt-ergo-2.0.0/alt-ergo-2.0.0.tar.gz
$ tar xvfz alt-ergo-2.0.0.tar.gz
$ cd alt-ergo-2.0.0
Install its dependencies (some of which were already met when you were building why3)
$ sudo apt-get install ocplib-simplex-ocaml-dev
Build it and install it!
$ ./configure && make
$ sudo make install
This prover can be useful for very specific proofs, and again has to be built from source:
$ wget http://wwwlehre.dhbw-stuttgart.de/~sschulz/WORK/E_DOWNLOAD/V_2.0/E.tgz
$ tar xvfz E.tgz
$ cd E
$ ./configure && make
$ sudo make install
This is an older prover (related to CVC4), but it can still be useful sometimes. Because it's written in an older C++ version, it can be hard to compile. Thankfully, the developers distribute a binary version, so we can use that.
$ wget https://cs.nyu.edu/acsys/cvc3/releases/2.4.1/linux64/cvc3-2.4.1-optimized-static.tar.gz
$ tar xvfz cvc3-2.4.1-optimized-static.tar.gz
$ cd cvc3-2.4.1-optimized-static
$ sudo cp -R * /usr/local
Follow the same steps as before:
$ why3 config --detect
And, if you are a vim user, you will probably want the syntax highlighting:
$ cp -r /usr/local/share/why3/vim ~/.vim
Opam is a package manager often used by Ocaml programs. The following instructions were contributed by Job Cuppen and Robin van Straeten.
First, install some dependencies: GMP, GtkSourceView and pkg-config, and of course Opam.
$
brew install gmp pkg-config gtksourceview opam
Next, initialize opam. This will create a .opam directory in your home folder:
$
opam init
This can take a while, so be patient.
Next, you are ready to install Why3 and Alt-Ergo via Opam:
$
opam install why3 why3-ide alt-ergo
Most provers are happily available via homebrew as well, so installing E prover, and Z3 can be done using:
$
brew install z3 eprover
For CVC4, you can use the command:
$ brew tap cvc4/cvc4
Followed by:
$ why3 install cvc4/cvc4/cvc4
Note that this may takes some time.
For CVC3, the instructions are similar to Linux, except that you download the OS X binary instead:
$ wget https://cs.nyu.edu/acsys/cvc3/releases/2.4.1/macosx/cvc3-2.4.1-macosx-optimized-static.tar.gz
$ tar xvfz cvc3-2.4.1-macosx-optimized-static.tar.gz
$ cd cvc3-2.4.1-macosx-optimized-static
$ sudo cp -R * /usr/local
Note that you may need to add the $HOME/.opam/default/bin directory to your path. This should be done by the
command:
\( eval \)(opam config env)
Let Why3 find the provers:
$ why3 config --detect
Note that you will have to run why3 ide from a terminal window. Also, because it uses a GTK2
library, it will look like it came from yesteryear.