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

Lukas Bulwahn bulwahn at in.tum.de
Mon Sep 12 16:40:31 CEST 2011

On 09/09/2011 02:52 PM, Makarius wrote:
> On Fri, 9 Sep 2011, Lukas Bulwahn wrote:
>> In my concrete case:
>> When running the compilation within the make command, I get:
>> *** exception Option raised
>> Exception- TOPLEVEL_ERROR raised
>> *** ML error
>> Whereas running it interactively in PG:
>> *** exception Match raised
>> *** At command "code_reflect"
>> The Match raised is the real reason for the exception in my case, and 
>> the one I was expecting.
>> The Option raised exception seems to caused somehow as a consequence 
>> of the previous exception within the non-interactive run.
> There can be a variety reasons for that.  Historically, the tty loop 
> (that is still used in PG) always had slightly different ideas about 
> command execution than the regular batch mode.  Since a couple of 
> years, I am trying to unify this in the new interactive document mode, 
> but we are not there yet.  (At the moment the latter is just a third 
> variant.  What does your example do in Isabelle/jEdit?)
> Another difference is sequential vs. parallel execution.  Passing 
> things through the future farm can influence exception behaviour in 
> certain ways, although ML user code can be written to be well-defined 
> in this respect.
> 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.
>     Makarius

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.


More information about the isabelle-dev mailing list