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

[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 create accounts for anybody from the broy network, who wants to 
access vmbroy9 for testing (4 core Windows 2008 virtual server, with full 
RDP terminal service, no ssh).


 	Makarius