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

[Makarius]

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