On 22/12/2016 08:02, Ralf Treinen wrote: > Hi Mehdi, > > On Thu, Dec 22, 2016 at 12:06:15AM +0100, Mehdi Dogguy wrote: >> Hi Ralf, >> >> On 21/12/2016 21:03, Ralf Treinen wrote: >>> how do you know that why will not be part of stretch ? >>> >> >> Why has been removed from testing since 2016-02-14 and why3 is now part >> of Stretch. I have assumed the former has been dropped in favor of the >> latter. Apologies if this is not the case. I'd be happy to restore the >> Recommends statements if that's useful for someone. > > this is not the case. Since the 2.36 upstream release of why, why > only contains the krakatoa and jessie plugins for frama-c. These now > generate code in the why3 language, which has to be proven using why3. > Only the "why" binary itself has gone. That is, why now depends both > on frama-c and why3. >
Thanks for the explanation! > The reasons for the removal of why from testing where different ones, > and should be fixed now. why 2.36-3 should migrate back into testing > in the next days. > It needs (at least) to be recompiled against the latest frama-c before being considered a candidate for migration. I've scheduled a binNMU on amd64 to see if it builds. I'll investigate the breakage if it fails. Regards, -- Mehdi
