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.
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
