[isabelle-dev] Nitpick-induced Isatest failures on "macbroy2"

[Jasmin Christian Blanchette]

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