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. Jasmin _______________________________________________ Isabelle-dev mailing list [email protected] https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
