[isabelle-dev] Option raised errors hides other error failures
Makarius
makarius at sketis.net
Fri Sep 9 14:52:33 CEST 2011
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
More information about the isabelle-dev
mailing list