[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?