Re: [why3] dropping coq support ?

[Stéphane Glondu <glondu@debian.org>]

Hello Ralf,

Le 14/03/2022 à 19:50, Ralf Treinen a écrit :
> 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?

I share your analysis and your conclusion.


Cheers,

-- 
Stéphane