[isabelle-dev] Option raised errors hides other error failures

[Makarius]

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 
>> leaves).
>> 
>> I am myself curious to see what is the cause of this particular 
>> breakdown.
>
> 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 
source text?


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.


 	Makarius