[isabelle-dev] moving isatest to poly 5.4

[Gerwin Klein]

On 29/12/2010, at 5:42 AM, Makarius wrote:

> On Mon, 20 Dec 2010, Andreas Lochbihler wrote:
>> 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,

Sorry, I've been dropping the ball on this before the holidays and am still on vacation until 5.1. 


> 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

Thanks, that will be very helpful.


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

Even though it seems I've misinterpreted Andreas' problem, Florian seems to confirm flakiness of 5.3 on large sessions which I've seen myself as well (it's the reason we're still running Isabelle2009-1). The problem seems to be somewhere in the memory allocation part of polyml, at least that is what is reporting exceptions (in C, not ML). No reason to drop support for 5.3 entirely, though, most people won't see the problems.

I propose we leave most of isatest on 5.3 and run mac-poly64-M4 (which is what AFP is based on) on your unofficial 5.4 and see how it's going. This should give us testing for both versions on Isabelle and for 5.4 on the AFP. 

I can do the switch when I'm back to the office.

Florian, I don't suppose there is an easy workaround in the code generator for Andreas' problem above? (Not that I can see why this code should not compile).

Cheers,
Gerwin