If the procedure does not work for you and that your machine has a standard configuration, please report the problem to arthur.chargueraud /@/ inria /./ fr so that I may update the procedure.

This document gives some hints on how to install Why3, as well as the automated provers Alt-ergo, CVC3, CVC4, and Z3, and the Coq proof assistant. For additional information, we refer to the Why3 official documentation.

There is a detailed tutorial for Ubuntu, and a mini-tutorial for Mac. If you have an exotic system (including Windows), it will save you a lot of trouble to install Ubuntu either natively or using VirtualBox or Docker.

Installation on Ubuntu

This tutorial was tested on an Ubuntu 14.04 distribution, on a 64-bit machine. It will most likely work just as well on a more recent Ubuntu release. For other Linux-based environments, you may need to adapt the command lines.


We assume the existence of a temporary folder (e.g. ~/softs) where to download and compile all the software.

   mkdir ~/softs
   cd ~/softs

Installation of Why3 and Alt-ergo

Using OPAM is probably the easiest route, but it might take longer because OPAM likes to recompile from sources.

Installation using OPAM

DO NOT install the OPAM ubuntu package because it is broken (as explained here), and because it might cause big trouble if you later want to install packages having OCaml has dependency.

Step 1: It appears that OPAM needs ocaml for its initialization. Install it on your system if you don't have it.

   sudo apt-get install ocaml

Step 2: Make sure you have a recent version of OPAM. Install version 1.2.0 either using the binary installer, or by compiling from the sources. The simplest way to get it all set up is to run the commands shown below:

   sudo wget https://raw.github.com/ocaml/opam/master/shell/opam_installer.sh -O - | sh -s /usr/local/bin/

More detailed instructions on how to install OPAM can be found here.

Step 3: When configuring OPAM as shown below, answer "Y" when ask if you want OPAM to modify "~/.bashrc" and "~/.ocamlinit".

  opam init
    # type 'enter' if asked for HTTP source

  eval `opam config env`

Step 4: You need to install at least one version of OCaml through OPAM, otherwise you will need to manually install many OCaml system packages as described in the section "Installation without OPAM". To install latest version of OCaml (this may take a while), run :

  opam switch 4.02.3
  eval `opam config env`   # not needed if still in the same terminal
  which ocamlc             # should be: /home/yourname/.opam/4.02.3/bin/ocamlc

Step 5: You need to install several system packages. They can be installed as follows.

  sudo apt-get install libgmp-dev libgtksourceview2.0-dev m4

Step 6: Install the Why3 and the Alt-ergo package (it takes some time, because everything is recompiled from source).

  opam install why3 alt-ergo
  why3 --version
  alt-ergo -version

After installing all the provers, you'll need to run "why3 config --detect-provers" as described in the section "Completing the installation" further in this document.

Installation without OPAM

Follow these instructions if you want to install Why3 and Alt-ergo from sources, without using OPAM.

First, you need to install OCaml and Menhir with the appropriate libraries.

   sudo apt-get install ocaml ocaml-native-compilers
   sudo apt-get install liblablgtk2-ocaml-dev liblablgtksourceview2-ocaml-dev libocamlgraph-ocaml-dev menhir

Remark: the package ocaml-native-compilers is recommended for faster compilation but not mandatory; the package libocamlgraph-ocaml-dev is optional (it is only required for hypothesis selection).

Then, we are ready to download, compile and install Why3. Make sure that the "configure" tells you that everything is ok during the process.

   wget https://gforge.inria.fr/frs/download.php/file/35214/why3-0.87.2.tar.gz
   tar -xzf why3-0.87.2.tar.gz
   cd why3-0.87.2/
   sudo make install
   cd ..

Now, to install alt-ergo, download the file called "Linux x86_64 binary" from here into the ~/softs folder. Then:

   sudo cp alt-ergo-static-0.99.1-x86_64 /usr/local/bin/alt-ergo
   sudo chmod +x /usr/local/bin/alt-ergo
   alt-ergo -version

Installation of CVC3

Use the commands below to install "64-bit Linux static library and executable" (available from here):

   wget http://www.cs.nyu.edu/acsys/cvc3/releases/2.4.1/linux64/cvc3-2.4.1-optimized-static.tar.gz
   tar -xzf cvc3-2.4.1-optimized-static.tar.gz
   sudo cp -R cvc3-2.4.1-optimized-static/* /usr/local/
   cvc3 -version

Remark: if you try to compile CVC3 from sources, it's likely that you'll need the package called "libgmp10".

Installation of CVC4

Use the commands below to install "Linux x86_64 binary" (available in the "Stable versions" column from here):

   wget http://cvc4.cs.nyu.edu/builds/x86_64-linux-opt/cvc4-1.4-x86_64-linux-opt
   sudo cp cvc4-1.4-x86_64-linux-opt /usr/local/bin/cvc4
   sudo chmod +x /usr/local/bin/cvc4
   cvc4 --version

Installation of Z3

Use the commands below to install Z3 (available from here):

   wget https://github.com/Z3Prover/z3/releases/download/z3-4.4.1/z3-4.4.1-x64-ubuntu-14.04.zip
   unzip z3-4.4.1-x64-ubuntu-14.04.zip
   sudo cp z3-4.4.1-x64-ubuntu-14.04/bin/z3 /usr/local/bin
   sudo chmod +x /usr/local/bin/z3
   z3 -version

Installation of Coq

Coq can be used to discharge Why3 proof obligations as well. If Coq is installed, then Why3 will be able to detect it during its configuration.

Intallation using system packages

For installation from packages, use:

   sudo apt-get install coqide
   coqc -version

Intallation using OPAM

Coq can also be installed from OPAM, although it takes a lot of time, because OPAM recompiles Coq and all of the standard library from the sources.

   eval `opam config env`  # only needed if you changed terminal
   opam install coq
   coqc -version

Completing the installation and testing

First, we ask Why3 to detect the freshly-installed provers.

   eval `opam config env` # only needed if you changed terminal
   why3 config --detect
   why3 --list-provers

If everything went well, you should see:

   Found prover Alt-Ergo version 0.99.1, Ok.
   Found prover CVC4 version 1.4, Ok.
   Found prover CVC3 version 2.4.1, Ok.
   Found prover Z3 version 4.4.1, Ok
   # possibly also with Coq (8.4pl3).

Then, you are ready to open the project. Assuming it is located in ~/whyproject, do:

   cd ~/whyproject
   why3 ide closestpair.mlw &

Installation on Mac

This installation procedure was reported by a kind user. Please don't hesitate to suggest variants or improvements.

First, install OCaml and related package (gtkglext might not be needed, I am not sure).

   brew install opam ocaml
   brew install gtkglext
   brew install gtksourceview

Then, add to bash_profile:

   export PKG_CONFIG_PATH=/usr/X11/lib/pkgconfig/:/usr/local/lib/pkgconfig:/usr/local/opt/libxml2/lib/pkgconfig/

Finaly, use OPAM to install the remaining tools:

   opam init
   opam config setup -a
   opam install alt-ergo
   opam install ocamlgraph
   opam install why3

For the installation of provers, follow the instruction from the Ubuntu tutorial above.