[isabelle-dev] moving isatest to poly 5.4

[Andreas Lochbihler]

 > On 17/12/2010, at 10:03 PM, Makarius wrote:
 >> On Fri, 17 Dec 2010, Gerwin Klein wrote:
 >>> Andreas Lochbihler pointed out that the AFP test is still running polyml 
version 5.3 as is most of isatest.
 >>>
 >>> Any arguments against moving all of this to polyml 5.4?
 >> Well, we do not have an official stable Poly/ML 5.4 for Isabelle yet.
 >>
 >> 5.4 has a problem with bigints in certain situations, so it would need at 
least one extra patch from the SVN.
 >
 >> So far I did not find time for looking more closely, and official Poly/ML 
5.3 is sufficiently stable.
 >
 > Well, no, it's not, that's the whole point. It's been flaky with concurrency 
and current Isabelle, not so much for small sessions, but certainly for big 
ones. According to Andreas, after his changes to JinjaThreads, the AFP test 
crashes more often than not on his local machine with poly 5.3, but works fine 
with poly 5.4.
No, it has nothing to do with stability and concurrency. Poly 5.3 crashes always 
because the @{code} antiquotation (for automatically testing the code generator 
setup) generates some code that makes the internal compiler of poly 5.3 crash.
Florian kindly figured that out for me a few weeks ago, so I moved to 5.4 where 
the problem no longer occurs.

The problem essential boils down to two SML datatype declarations

datatype 'a T = T of ('a * 'a T) list;
datatype 'a S = S of 'a T;

When they are fed incrementally to PolyML 5.3, it crashes with

Exception- InternalError: changeL: Unknown code raised while compiling


 > He's holding back pushing his change, because he's afraid it will just fail 
all the time.
Meanwhile, I decided to temporarily comment out the the code generator test and 
push my changes.

BTW, I have given up on running JinjaThreads in parallel. With 16GB of memory on 
my local machine, I have not seen any stability problems (in mode "-M 1") for 
months.

Andreas