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.