Previous Up Next

Chapter 5  Compilation, Installation

In short, installation proceeds as follows.

make install
(as super-user)

5.1  Installation Instructions from Source Distribution

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


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 specific Coq features, i.e. the Coq tactic 10 and Coq realizations 9, 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.

When configuration is finished, you can compile Why3.


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

make install

Installation can be tested as follows:

  1. install some external provers (see Section5.4 below)
  2. run why3config --detect
  3. run some examples from the distribution, e.g. you should obtain the following:
    $ cd examples
    $ why3replayer scottish-private-club
    Info: found directory 'scottish-private-club' for the project
    Opening session... done
    Progress: 4/4
    Everything OK.
    $ why3replayer programs/same_fringe
    Info: found directory 'programs/same_fringe' for the project
    Opening session... done
    Progress: 12/12
    Everything OK.

5.2  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

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

5.3  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)

5.4  Installation of 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 these provers before compiling and installing Why.

For installation of external provers, please refer to the specific section about provers on the Web page

For configuring Why3 to use the provers, follow instructions given in Section 6.1.

5.5  Multiple Versions of the Same Prover

Since version 0.72, Why3 is able to use several versions of the same prover, e.g. it can use both CVC3 2.2 and CVC3 2.4.1 at the same time. The automatic detection of provers looks for typical names for their executable command, e.g. cvc3 for CVC3. However, if you install several version of the same prover it is likely that you would use specialized executable names, such as cvc3-2.2 or cvc3-2.4.1. To allow the Why3 detection process to recognize these, you can use the option --add-prover to why3config, e.g.

why3config --detect --add-prover cvc3-2.4 /usr/local/bin/cvc3-2.4.1

the first argument (here cvc3-2.4) 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 11.2 for details.

5.6  Session Update after Prover Upgrade

If you happen to upgrade a prover, e.g. installing CVC3 2.4.1 in place of CVC3 2.2, 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, you will be asked to choose between 3 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-archive 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.

Outside the GUI, the prover upgrades are handled as follows. The why3replayer tool will just ignore proof attempts marked as archived. Conversely, a non-archived proof attempt with a non-existent prover will be reported as a replay failure. The tool why3session allows you to perform move or copy operations on proof attempts in a fine-grain way, using filters, as detailed in Section 6.6.

Previous Up Next