--- layout: fc_discuss_archives title: Message 24 from Frama-C-discuss on July 2012 ---
Hello, 2012/7/10 Jens Gerlach <jens.gerlach at first.fraunhofer.de>: > attached are some installation notes of mine for WP (in German-). > If you find a a simpler way then please tell me. > (They are for nitrogen, but currently I am using the nitrogen package that comes with ubuntu 2012-04.) > > Regarding the circular dependency, I understood the issue as follows: > WP can use alt-ergo directly (without why). To use other provers you have to install why first. > For details see our installation notes. > That's right, Why is only needed by WP at run-time (and if you intend to use something other than alt-ergo or Coq). Regarding your installation notes, as far as I know, one of the install of WP-0.5 is, as you guessed, unnecessary, as well as the second install of Frama-C. In other words, - Frama-C needs to be installed before Why2 and WP-0.5 - Why3 and alt-ergo can be installed completely separately Best regards, -- E tutto per oggi, a la prossima volta Virgile