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
_______________________________________________
isabelle-dev mailing list
[email protected]
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
