uuomul at yahoo.com
Thu May 15 20:55:39 CEST 2014
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.)
On Thursday, May 15, 2014 8:32 PM, Jasmin Christian Blanchette <jasmin.blanchette at gmail.com> wrote:
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.
More information about the isabelle-dev