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

[Jasmin Christian Blanchette]

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")
>> 
>> "remote_vampire": Try this: by metis (12 ms).
>> "remote_e_sine": Try this: by metis (13 ms).
> 
> 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).

Jasmin