[isabelle-dev] "Exception." fun oddity in Isabelle 2009-2
makarius at sketis.net
Mon Dec 6 16:15:19 CET 2010
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.
After Isabelle2009-2 such indirect interrupts are propagated to the
surface more clearly. You cannot really handle such low-level system
More information about the isabelle-dev