[isabelle-dev] AFP

[Andrei Popescu]

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.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.

Jasmin