Previous Up Next

Chapter 4  Compilation, Installation

4.1  Installing Why3

4.1.1  Installation via OPAM

The simplest way to install Why3 is via OPAM, the OCaml package manager. It is as simple as

> opam install why3

Then jump to Section 4.2 to install external provers.

4.1.2  Installation Instructions from Source Distribution

In short, installation from sources proceeds as follows.

> ./configure
> make
> make install
(as super-user)

After unpacking the distribution, go to the newly created directory why3-1.0.0. Compilation must start with a configuration phase which is run as

> ./configure

This analyzes your current configuration and checks if requirements hold. Compilation requires:

For some of the Why3 tools, additional OCaml libraries are needed:

If you want to use the Coq realizations (Section 8.2), then Coq has to be installed before Why3. Look at the summary printed at the end of the configuration script to check if Coq has been detected properly. Similarly, in order to use PVS (Section 8.5) or Isabelle (Section 8.4) to discharge proofs, PVS and Isabelle must be installed before Why3. You should check that those proof assistants are correctly detected by the configure script.

When configuration is finished, you can compile Why3.

make

Installation is performed (as super-user if needed) using

make install

Installation can be tested as follows:

  1. install some external provers (see Section 4.2 below)
  2. run why3 config --detect
  3. run some examples from the distribution, e.g. you should obtain the following (provided the required provers are installed on your machine):
    $ cd examples
    $ why3 replay logic/scottish-private-club
     1/1 (replay OK)
    $ why3 replay same_fringe
     18/18 (replay OK)
    

Local Use, Without Installation

It is not mandatory to install Why3 into system directories. Why3 can be configured and compiled for local use as follows:

./configure --enable-local
make

The Why3 executables are then available in the subdirectory bin/. This directory can be added in your PATH.

Installation of the Why3 API

By default, the Why3 API is not installed. It can be installed using

make byte opt
make install-lib
(as super-user)

4.2  Installing External Provers

Why3 can use a wide range of external theorem provers. These need to be installed separately, and then Why3 needs to be configured to use them. There is no need to install automatic provers, e.g. SMT solvers, before compiling and installing Why3. For installation of external provers, please refer to the specific section about provers from http://why3.lri.fr/. (If you have installed Why3 via OPAM, note that you can install the SMT solver Alt-Ergo via OPAM as well.)

Once you have installed a prover, or a new version of a prover, you have to run the following command:

> why3 config --detect

It scans your PATH for provers and updates your configuration file (see Section 5.1) accordingly.

4.2.1  Multiple Versions of the Same Prover

Why3 is able to use several versions of the same prover, e.g. it can use both CVC4 1.4 and CVC4 1.5 at the same time. The automatic detection of provers looks for typical names for their executable command, e.g. cvc4 for CVC3. However, if you install several versions of the same prover it is likely that you would use specialized executable names, such as cvc4-1.4 or cvc4-1.5. If needed, option --add-prover can be added to the config command to specify names of prover executables, e.g.

why3 config --add-prover cvc4 /usr/local/bin/cvc4-dev

the first argument (here cvc4) must be one of the class of provers known in the file provers-detection-data.conf typically located in /usr/local/share/why3 after installation. See Appendix 9.2 for details.

4.2.2  Session Update after Prover Upgrade

If you happen to upgrade a prover, e.g. installing CVC4 1.5 in place of CVC4 1.4, then the proof sessions formerly recorded will still refer to the old version of the prover. If you open one such a session with the GUI, and replay the proofs, a popup window will show up for asking you to choose between three options:

Notice that if the prover under consideration is an interactive one, then the copy option will duplicate also the edited proof scripts, whereas the upgrade-without-copy option will just reuse the former proof scripts.

Your choice between the three options above will be recorded, one for each prover, in the Why3 configuration file. Within the GUI, you can discard these choices via the Preferences dialog: just click on one choice to remove it.

Outside the GUI, the prover upgrades are handled as follows. The replay command will take into account any prover upgrade policy stored in the configuration. The session command performs move or copy operations on proof attempts in a fine-grained way, using filters, as detailed in Section 5.5.


Previous Up Next