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