[why3] dropping coq support ?

[Ralf Treinen <treinen@fdn.fr>]

Hello,

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
  architectures.

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.