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
Makarius
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
