[isabelle-dev] AFP continously broken

Jasmin Christian Blanchette jasmin.blanchette at gmail.com
Thu Feb 27 19:25:15 CET 2014

Am 26.02.2014 um 19:26 schrieb Makarius <makarius at sketis.net>:

> In the past few days AFP has been continuously broken: presently AFP/3fc9e6ace21f and Isabelle/1f27d75ccf05. After some time in a bad state it becomes increasingly difficult to guess which changes are responsible. http://isabelle.in.tum.de/reports/Isabelle/shortlog provides some clues, but they are unsure: it looks like lifting, codegen,

The failure in the "Coinductive" entry appears to have been introduced by Isabelle/f1ed1e9cd080, a change to the lifting package. The responsible developer now knows about it.

>  potentially codatatype.

I doubt so. I tested the last wave of big (co)datatype-related changes thoroughly, to the extent that this was possible with an already broken AFP. But we'll see once the dust settles.


More information about the isabelle-dev mailing list