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