makarius at sketis.net
Thu May 15 21:03:47 CEST 2014
On Thu, 15 May 2014, Jasmin Christian Blanchette wrote:
> 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.
That's me. It is a trivial breakdown due to one of my recent Pure
cleanups. I have updated that in AFP/ed0dfdd2b00d.
We also have a total failure of existence with isatest, since HOL-Proofs
does not build on the initial test machine (lxbroy2) for the documentation
sessions. I still need to find out if it is the one lemma addition by
Tobias, my change of Poly/ML, or just that machine which is constantly
running some boring batch process: on all cores: 178027:57 diam_5
More information about the isabelle-dev