Previous Up Next

Chapter 4  Appendices

4.1  Requirements

Compiling from sources requires Objective Caml compiler, version 3.09 or higher.

External theorem provers must be installed. See the page

For using the Coq interactive prover, you need Coq version 8.0 or higher.

4.2  Installation procedure

4.2.1  From the sources

Get a copy of sources at the web page

Decompress the archive in a directory of your choice.

Run commands

make install

4.2.2  Binaries

Please look at the web page for binaries for popular architectures. Krakatoa is distributed as part of the Why debian package, available on standard repositories of debian-based distributions.

4.3  Summary of features and known limitations

4.4  Contacts

The webpage for Krakatoa is at URL and the webpage for the Why platform in general is at

For general questions regarding the use of the tool, please use the Why mailing list. You need to subscribe to the list before sending a message to it. To subscribe, follow the instructions given on page

For bug reports, please use the bug tracking system at For security reasons, you need to register before submitting a new bug. Please create an account there, where you can put "ProVal" for the required field "INRIA Research Project you work with or work in".

In case if the mailing list above is not appropriate, you can contact the authors directly at the following address: mailto:Claude dot Marche at inria dot fr.

Previous Up Next