Compiling from sources requires Objective Caml compiler, version 3.09 or higher.
External theorem provers must be installed. See the page http://why.lri.fr/provers.html
For using the Coq interactive prover, you need Coq version 8.0 or higher.
Get a copy of sources at the web page http://why.lri.fr/.
Decompress the archive in a directory of your choice.
./configure make make install
Please look at the web page http://why.lri.fr/ for binaries for popular architectures. Krakatoa is distributed as part of the Why debian package, available on standard repositories of debian-based distributions.
The webpage for Krakatoa is at URL http://krakatoa.lri.fr/ and the webpage for the Why platform in general is at http://why.lri.fr.
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 http://lists.gforge.inria.fr/cgi-bin/mailman/listinfo/why-discuss
For bug reports, please use the bug tracking system at https://gforge.inria.fr/tracker/?atid=4012&group_id=999&func=browse. 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.