[isabelle-dev] "Exception." fun oddity in Isabelle 2009-2

[Lucas Dixon]

On 06/12/2010 15:15, Makarius wrote:
> On Sun, 5 Dec 2010, Lucas Dixon wrote:
>
>> While playing around with a robotic horror that throw strange monsters
>> at the function package, I came across this rather strange error...
>>
>> My guess is that some accidental infinite loop makes something bad
>> happen at a low level... but I've ever seen the "Exception." things
>> before, so I'm not too sure what to do next.
>>
>> Moreover, (and importantly for me) when I'm calling this from ML, I'm
>> not sure how to catch the resulting error, it seems to be skipping
>> past my attempts to handle it. Any thoughts?
>
> In Isabelle2009-2, the failure that is printed as "Exception" means that
> some of the futures to do proofs in the background has somehow been
> canceled, e.g. by running out of resources.

thanks! that was my suspicion.

> After Isabelle2009-2 such indirect interrupts are propagated to the
> surface more clearly. You cannot really handle such low-level system
> failures, though.

... at the moment I need Isabelle2009-2, too many dependencies to 
quickly unravel... is there an easy way to disable 
multi-threading/futures so that I can see what the real ML error is? a 
quick pointer to what to hack in the ML-Systems dir? :)

At the moment I need reliability/simplicity over speed; so will probably 
need to do this anyway...

cheers,
lucas

-- 
The University of Edinburgh is a charitable body, registered in
Scotland, with registration number SC005336.