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
