Bug#813596: coq-float and why cannot be built with Coq 8.5 (Bugs #813596 and #815684)
Hello,
On Sat, Jul 23, 2016 at 01:32:57PM -0400, Nicolas Braud-Santoni wrote:
> coq-float and why cannot build under Coq 8.5, leading to two FTBFS bugs.
> (Note: This is about why, not why3)
>
> I confirmed that (beyond some mild build-system breakage) the issues
> are due to changes in Coq, and neither are still maintained upstream.
>
> As such, I would like to suggest we delete those packages:
> they are not buildable anymore, are not maintained anymore,
> and taking up maintainership ourselves sounds like a losing proposal.
Why also does not compile with the current vesion of why3. I talked
to why upstream about this a few days ago. There will be a new upstream
release of why soon which will fix this. I suspect this will also
fix compilation whith coq-8.5.
I also asked him whether it stills makes sense to maintain a package
for why and was told that yes, since why3 does not yet support
interfaces to frama-c and krakakoa.
I don't know about coq-float, though.
-Ralf.
Reply to: