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

Makarius makarius at sketis.net
Tue Apr 24 20:58:58 CEST 2012

On Tue, 24 Apr 2012, Jasmin Christian Blanchette wrote:

> Am 23.04.2012 um 22:02 schrieb Makarius:
>> On Mon, 23 Apr 2012, Alexander Krauss wrote:
>>> Sledgehammering...
>>> "spass": Internal error:
>>> exception Empty raised (line 458 of "library.ML")
>> I've seen it before, but for the remote provers, and did not 
>> investigate further yet. My first idea was it could be a problem of the 
>> network connection of the heavily fortified vmbroy9 machine, but spass 
>> is certainly local.
> I can reproduce it on my WinXP-on-VirtualBox installation. There are a 
> couple of variants of this: Sometimes it affects a remote prover, 
> sometimes I get an "empty string" error from "remote_e". It's certainly 
> not tied to "spass". The error seems to go away when an explicit prover 
> is specified by passing "[prover = ...]" to the "sledgehammer" command.
> I'll see if I can debug this further. I can't seem to get this to happen 
> with the Mac bundle (from 23 April 2012).

I have also made some more experiments.  The Empty exception is from the 
split_last here 
where you don't get any output unexpectedly, bacause /bin/sh has crashed. 

Such things happen on Cygwin.  I will try to sort out the physical 
problem.  Maybe you can make the ML part more informative nonetheless.


More information about the isabelle-dev mailing list