[isabelle-dev] AFP

[Jasmin Christian Blanchette]

Am 15.05.2014 um 18:59 schrieb Tobias Nipkow <nipkow at in.tum.de>:

> Very good question. This is and has been the situation for a week or so:
> 
> [Tycon] is still on FAIL.
> [Nominal2] is still on FAIL.
> [Incompleteness] is still on FAIL.
> [HyperCTL] is still on FAIL.
> [Launchbury] is still on FAIL.
> 
> Could the parties concerned let us know what is going on?

I don't believe (and hope not) to be one of the interested parties, but it may be useful to point out that there were, from what I can recall, at least three distinct waves of failures.

1st wave: HyperCTL. This formalization has never worked against the repository version of Isabelle. Andrei is aware of this.

2nd wave: Nominal2, Incompleteness, Launchbury. Here I didn't investigate much, but from the Nominal2 failure I get the impression that some Pure ML signature has been changed.

3rd wave: Tycon. Change Isabelle/952833323c99 appears to be connected.

Jasmin