search

OCamlPro / owi

WebAssembly Swissknife & cross-language bugfinder
https://ocamlpro.github.io/owi/
GNU Affero General Public License v3.0
136 stars 17 forks source link

try to reduce the dependencies needed for e-acsl #428

Open zapashcanon opened 1 month ago

zapashcanon commented 1 month ago

Currently, there's no opam package only for e-acsl but one has to install the whole frama-c package. It means we are installing why3 for instance, which we will never need. It would be good make the installation of e-acsl lighter (for instance, why3 could be made an optional dependency of frama-c ?).

We should probably discuss this with @signoles.

AllanBlanchard commented 1 month ago

We cannot make Why3 an optional dependency. By doing this, the default installation of Frama-C would not embed WP which is one of the plug-ins that are used the most in Frama-C. We do not want to create specific packages for Frama-C plug-ins (even the main ones) because it would pollute Opam.

However, it is already possible to compile Frama-C by hand with Why3 : if the dependency is not there, the WP plug-in will not be compiled and that's all. If you really need it we can also provide a custom opam file that does not embed the Why3 dependency.