Am 15.05.2014 um 18:59 schrieb Tobias Nipkow <nip...@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 _______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
