[isabelle-dev] Nitpick-induced Isatest failures on "macbroy2"
Jasmin Christian Blanchette
jasmin.blanchette at gmail.com
Wed Mar 24 16:09:06 CET 2010
A quick followup on the "macbroy2" failures.
The original failures, which prompted me to write to the list, were on
the ML platform "x86_64-darwin" with Mac OS 10.6 (macbroy2). I solved
the problem quickly back then, but since Saturday we've been
experiencing the same failures on "x86-darwin" on 10.6. It turns out
the problem was exactly the same as I could have guessed two weeks ago
by thinking a bit outside the box. I've now installed a new version of
Kodkodi, 1.2.12, that is set up in such a way that these failures
should not occur again.
The technical details: There seems to be a sporadic bug in the Mac OS
10.6 32-bit implementation of the JVM. That bug has never manifested
itself on Mac OS 10.5 (which I use daily) or on the 10.6 64-bit JVM.
The new Kodkodi setup always uses the 64-bit JVM on 10.6, irrespective
of whether the ML platform is "x86-darwin" or "x86_64-darwin".
Incidentally, Nitpick also failed on all platforms on Monday. This was
due to a change of semantics of a basic Isabelle function that also
broke the Predicate Compiler -- i.e., it was a good thing that the
Nitpick tests caught this quickly.
Thanks for your patience.
More information about the isabelle-dev