[isabelle-dev] "spass": Internal error: exception Empty raised (line 458 of "library.ML")
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:
>>> "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
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