Concerning HyperCTL: I will fix this by Tuesday at 8:00 AM. (Sorry for delaying this.
I was extremely busy the last weeks, and did not get a chance to pull out the development version and fix the problem -- yes, to my shame, I am not using the development version.) Andrei On Thursday, May 15, 2014 8:32 PM, Jasmin Christian Blanchette <jasmin.blanche...@gmail.com> wrote: 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
