--- layout: fc_discuss_archives title: Message 68 from Frama-C-discuss on May 2010 ---
Boris Hollas a ?crit : > I will file a bug report/change request for the issue with #define and > const. OK. > For Boron, is it possible to provide a tarball that includes > - Frama-C > - Jessie > - why Yes it could be done since Why-2.26 is now released. > - Simplify At least one other Frama-C user complains off-list that Simplify is not a free software. I am not a lawyer but I guess the following sentence of the Simplify license prevents us to redistribute this tool within Frama-C: "You may download, modify and redistribute the software to individuals for personal, non-commercial purposes free of charge [...]" Anyway why including just a prover only useful for an external plug-in (even it is a major one)? If we follow this way, one day we will provide all existing (even non-free) provers and the transitive closure of all the requirements (including a linux kernel at the end?)... We have chosen a tractable limit by including only ocamlgraph within Frama-C since we usually require (at least) the last version of this library. All other requirements are not provided in the source distribution. > - a makefile We already provide a Makefile for Frama-C and another for Why. So you just have to do something like "./configure && make && sudo make install && cd why && ./configure && make && sudo make install". Thus I think that there is no really need to provide one additional not-so-easy-to-maintain Makefile. Ok Frama-C is an open source project: fill free to contribute ;-). > - installation instruction that lists additional required packages > for download on the frama-c site? Are the "compilation instructions" [1] not enough? [1] http://frama-c.com/install-boron-20100401.html -- Julien