OCamlPro
try to reduce the dependencies needed for e-acsl
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.
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.
We do not want to create specific packages for Frama-C plug-ins (even the main ones) because it would pollute Opam.
@AllanBlanchard, I don't think this is a problem for the opam repository and it would be really interesting for us (and probably many other projects). People won't complain if you publish many packages, for instance, there are 195 unique packages only for Tezos... My guess would be that splitting frama-c in many packages would lead to ten times less packages than what Tezos is doing.
Maybe someone such as @shonfeder, @mseri, @avsm or @kit-ty-kate can tell if having many packages instead of one has ever been a problem but I don't think so.
It is absolutely no problem to split your release to multiple packages, many other packages (probably even most of the larger ones) do this. As long as we don’t talk about hundreds of packages but a handful or two, the process is rather smooth.
Tezos and Janestreet are two special cases in the sense that their releases are usually huge, and we then ask them to try and submit them in small incremental batches, and the reviews take a lot more than smaller ones.
We will discuss this with the Frama-C team.
For us, it has a notable impact on various parts of our process and on the maintenance.
We are OK with the idea, although we have to find the right way to split Frama-C. However, there are a few technical difficulties to overcome.
- currently, there is no direct way to compile parts of Frama-C,
- we first need to remove the old GUI,
- we have to check how all of this interact with the new GUI.
And of course, we have to find resources to do that without breaking everything.
Great! I think this will help projects like Owi to more easily depends on parts on Frama-C and I'm glad to hear you are willing to go in this direction.
I think the rough idea is to:
- split the code in many dune libraries/executable if this is not the case already;
- make all of them distinct public libraries/executables, each with an associated dune/opam package;
- have a meta frama-c package/library that depends on all of them (and re-exports the various libraries to make the life of people that do not care to depend on everything easier).
I am not really familiar with the GUI part so I don't have much to say about it.
Is this close to what you are planning? I may be able to help a little bit if you have any questions or issues. :)
We already have the different dune packages, public libraries, etc (although most opam files are empty), and indeed what you list is basically what we should do.
However currently, the files are all dispatched along the directories hierarchy and I know that in the past we already had some trouble because of that when we enabled with the possibility of disabling plug-ins compilation even if all their dependencies are met. We have a horrible hack for that.
Currently, I do not know whether we will need help, it's purely a question of finding a time slot to do it and check that everything still works in developers workflow, in our CI, in Opam, etc.