--- layout: fc_discuss_archives title: Message 25 from Frama-C-discuss on July 2012 ---
Hi, Le 10/07/2012 17:14, Jens Gerlach a ?crit : > > Hier sind einige Notizen zur Installation von > Frama-C/WP, Frama-C/Jessie (why2 und why3) > f?r Linux. > > Erst einmal folgende Sachen installieren: > > sudo apt-get install ocaml ocaml-native-compilers graphviz \ > liblablgtksourceview2-ocaml-dev liblablgtk2-gnome-ocaml-dev > > Ausserdem habe ich folgende Pakete ueber Synaptic installiert: > alt-ergo, cvc3, ocamlgraph, coq So far so good, although I'm not the synpatic package are very up-to-date, I would recommend to install up-to-date version of provers > Mit Nitrogen beginnen und Frama-C/WP installieren lassen. > > cd frama-c-Nitrogen-20111001/ > ./configure > make > sudo make install > > Upgrade zu WP 0.5 (es reicht vermutlich auch, wenn man das nur am Ende macht) > > cd wp-0.5-Nitrogen-20111001 > autoconf > ./configure > make depend > make > sudo make install > > Frama-C/Jessie ueber why-2.30 installieren > > cd why-2.30/ > ./configure > make > sudo make install > > Noch einmal Frama-C installieren. > > cd frama-c-Nitrogen-20111001/ > ./configure > make > sudo make install I'm very surprised that the Jessie plugin will still work if you reinstall Frama-C a second time. A dynamic load error should occur... > Why3 installieren > > cd why3-0.71/ > ./configure > make > sudo make install Ach das ist nicht gut ! especially the next release of Why2 will require Why3 to be installed before. The right order should be 1) compile and install why3, configure it (why-config) and hopefully check the installation on examples/hello_proof.why 2) compile and install Frama-C. If WP is included and complains about why missing, it is probably not a problem (see Virgile answer) 3) compile Why2.30 that include the Jessie plugin, that requires both Why3 and Frama-C installed Hopefully the future version of WP plugin will use only Why3 anyway, so that should work without problem. If I am wrong, then a bug should be reported. - Claude -- Claude March? | tel: +33 1 72 92 59 69 INRIA Saclay - ?le-de-France | Universit? Paris-sud, Bat. 650 | http://www.lri.fr/~marche/ F-91405 ORSAY Cedex |