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