[isabelle-dev] "Exception." fun oddity in Isabelle 2009-2
ldixon at inf.ed.ac.uk
Mon Dec 6 18:55:10 CET 2010
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...
The University of Edinburgh is a charitable body, registered in
Scotland, with registration number SC005336.
More information about the isabelle-dev