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

[Makarius]

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 
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.


 	Makarius