Re: frama-c_20161101+silicon+dfsg-1_amd64.changes ACCEPTED into unstable
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
Reply to: