[Date Prev][Date Next] [Thread Prev][Thread Next] [Date Index] [Thread Index]

[why3] dropping coq support ?


since I have to stay at home for a few days I might as well use that for
picking up maintenance of some debian packages, for instance why3.

I am thinking of dropping coq support for why3. What makes the support
for coq so different from the support for other provers in why3 is that
- it makes why3 build-depend on coq
- it makes the binary package why3-coq depend on a particular version of coq
- it introduces quite some complexity into the why3 packages, partially
  (but not only) due to the fact that coq does not build on all release

Since coq support is tied to a particular version of coq, there always
is the problem that why3 upstream lacks behind coq upstream. The coq
team is aiming at a 6-month release cycle, and why3 major releases
usually take longer, and are not synchronized with coq. This means that
when coq is updated in debian one has to cherry-pick a patch for upgrading
coq-support from the why3 git - if it exists at all. For instance, currently
the lastest released version of why3 supports coq up to 8.13, there
is a patch in the git development branch for coq 8.14, and now we have
coq 8.15 in debian.

I do not see any better solution to keep up maintainability of why3
than to drop the coq support.

Do others on this list have any thoughts about that?

Cheers -Ralf.

Reply to: