MPRI

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-ergo
OPAM 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 -version
With 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


Page generated on 2024/3/7