[isabelle-dev] moving isatest to poly 5.4

Makarius makarius at sketis.net
Tue Dec 28 19:42:19 CET 2010

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:


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


More information about the isabelle-dev mailing list