If the procedure does not work for you and that your machine has a standard configuration, please report the problem to Claude.Marche /@/ 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, CVC4, and Z3, and the Coq proof assistant. For additional information, we refer to the Why3 official documentation.
The version of this document was written in December 2020 and is checked with the version 1.4.0 of Why3 and the prover versions Alt-Ergo 2.4.0, CVC4 1.7 and Z3 4.8.6. Using newer version of provers is usually OK.
The following instructions are expected to work on a computer with Linux operating system or under MACOS. The instructions are given in detail for Debian and Ubuntu Linux distributions, but should work similarly for other systems as above. If you have a more exotic operating system (such as Microsoft Windows), it will save you a lot of trouble to install Ubuntu either natively or using VirtualBox or Docker.
Installation of Why3 using OPAM
Using OPAM is probably the easiest route, but it might take longer because OPAM recompiles packages from sources.
Step 1: install and configure OPAM The first step is thus to install the OPAM system which can be done under Ubuntu as
sudo apt install opam
The apt tool is naturally supposed to install all required packages on which opam depends.
The next step is to configure OPAM as shown below. We recommend to 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 2:Install Why3 and Alt-Ergo Install the Why3 and its GTK ide, and the Alt-ergo package (it takes some time, because everything is recompiled from source).
opam install why3 why3-ide alt-ergoOPAM may ask you to install other packages from your distribution, such as gmp and gtk3. OPAM is good at recommending the appropriate command to do so, so we recommend to follow OPAM advices.
After installing is complete we recommend to check the versions using
why3 --version alt-ergo -versionWith the current OPAM you should get 1.4.0 and 2.4.0 respectively.
Installation of extra automatic provers
Installation of CVC4
Use the commands below to install "Linux x86_64 binary" (available in the "Stable versions" column from here):
wget https://github.com/CVC4/CVC4/releases/download/1.7/cvc4-1.7-x86_64-linux-opt sudo cp cvc4-1.7-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.8.6/z3-4.8.6-x64-ubuntu-16.04.zip unzip z3-4.8.6-x64-ubuntu-16.04.zip sudo cp z3-4.8.6-x64-ubuntu-16.04/bin/z3 /usr/local/bin sudo chmod +x /usr/local/bin/z3 z3 -version
After installing all the provers, you'll need to ask Why3 to detect your installed provers
why3 config detect why3 --list-provers
If everything went well, you should see:
Found prover Alt-Ergo version 2.3.0, Ok. Found prover CVC4 version 1.7, Ok. Found prover Z3 version 4.8.6, Ok.
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.
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.
opam install coq why3-coq coqc -version why3 config detect
Installation without OPAM
The procedure below is an old one that has been updated for a while. It is likely that several adaptations are required, in particular regarding the versions of the tools. Do not hesitate to report necessary updates to Claude.Marche /@/ inria /./ fr
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/38367/why3-1.3.3.tar.gz tar -xzf why3-1.3.3.tar.gz cd why3-1.3.3/ ./configure make sudo make install cd ..
To install alt-ergo without OPAM, see here