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.
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
Using OPAM is probably the easiest route, but it might take longer because OPAM likes to recompile from sources.
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.
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/ ./configure make 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
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".
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
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
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.
For installation from packages, use:
sudo apt-get install coqide coqc -version
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
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 &
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.