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

[Lukas Bulwahn]

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.


Lukas