[isabelle-dev] Option raised errors hides other error failures
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
> 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.
More information about the isabelle-dev