[isabelle-dev] "spass": Internal error: exception Empty raised (line 458 of "library.ML")

Jasmin Blanchette jasmin.blanchette at gmail.com
Tue Apr 24 21:05:25 CEST 2012

Am 24.04.2012 um 20:58 schrieb Makarius:

> have also made some more experiments.  The Empty exception is from the split_last here http://isabelle.in.tum.de/repos/isabelle/file/ea153f6abdb6/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML#l614 where you don't get any output unexpectedly, bacause /bin/sh has crashed. Ouch!
> Such things happen on Cygwin.  I will try to sort out the physical problem.  Maybe you can make the ML part more informative nonetheless.

OK, it looks like we came to the same conclusion (see my email from one minute ago).


More information about the isabelle-dev mailing list