[isabelle-dev] Option raised errors hides other error failures
makarius at sketis.net
Mon Sep 12 17:36:41 CEST 2011
On Mon, 12 Sep 2011, Lukas Bulwahn wrote:
>> In the concrete situation, above one needs to isolate the true reason
>> for the unexpected non-determinism. Either by bisection over the
>> history (induction over the construction of the sources) or by
>> investigating the current version at runtime, with Toplevel.debug,
>> exception_trace etc. in the usual way (this can be like reading tea
>> I am myself curious to see what is the cause of this particular
> I investigated the case a little bit more. It does occur with PolyML
> 5.2.1, but not with PolyML 5.3.0. Moving to PolyML 5.3.0 solves the
> issue for me, but there might be some other long-term users out there,
> still enjoying the 5.2.1 version.
Did you manage to get an exception trace that points to some piece of
Since this appears to be related to the code generator, I can also make
some educated guesses:
* Some genuine ML compiler problem -- Florian once exposed a few of them
when generating unusual code. David Matthews fixed these problems later,
but in 5.2.1 they are probably still present.
* Again a variation of the SML/NJ environment problem where structure
"Code" was re-used. In 5.2.1 there is no ML environment management within
the theory, just like SML/NJ. These very important ML management things
were introduced by David Matthews in 5.3.0.
In principle we still support 5.2.1 officially, but it is probably of
little practical signifance for end-users. (Old compilers often help
bisecting very old problems in the history.) The official distribution
will use 5.4.0 again, unless David Matthews happens to release a newer
version within the next 2 weeks.
More information about the isabelle-dev