[isabelle-dev] moving isatest to poly 5.4

[Makarius]

On Mon, 20 Dec 2010, Andreas Lochbihler wrote:

>> 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

I am not sure what is the conclusion of this thread concerning the AFP 
build setup, but here is a distribution of Poly/ML 5.4 that is very likely 
to be the official one for the coming release in January 2011:

   http://www4.in.tum.de/~wenzelm/unofficial/polyml-5.4.0.tar.gz

This does not mean that Poly/ML 5.3.0 is discontinued for Isabelle itself, 
of course.


 	Makarius