search

Stevendeo / Pilat

Invariant generator for polynomial loops
GNU Lesser General Public License v2.1
8 stars 2 forks source link

Add compatibility constraints for Frama-C versions #1

Closed maroneze closed 2 years ago

maroneze commented 6 years ago

The latest Frama-C release (Chlorine) is incompatible with pilat 1.1. I added a constraint in the opam file, but it is not enough: opam is still able to find an old release (2014) and tries to install it, and them pilat, but fails miserably.

I would recommend checking the oldest release of Frama-C that should be compatible with pilat and blacklisting those older than that, to avoid opam from being able to find exotic package combinations.

Otherwise, you might consider adding a strong depends constraint with the exact Frama-C version that is known to be compatible with your plug-in. It's a bit excessive, but at least prevents your users from getting installation errors. You can then whitelist new releases as they come, if they remain compatible.

Stevendeo commented 6 years ago

Thank you for the feedback. I think I will go for your second idea for now so that I am sure that people who wants to use pilat can do it easily. As my current version of pilat currently works on Chlorine, I will set the constraint on this when it is available on Opam.

maroneze commented 6 years ago

Thanks! If you can, please update both the constraints on the old version (1.1, to avoid build fails in opam's CI) and in the new one.

Stevendeo commented 6 years ago

Oh ok I will do it. Do you think opam checks dependencies of every old versions of packages ?

maroneze commented 6 years ago

It usually does, I did some backporting of constraints on older releases of Frama-C some time ago because of that. Unfortunately the Opam Weather Service no longer seems to work and I don't recall if there is another place where we can see all builds, but there used to be a huge table with several versions of packages tested, including older ones.