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
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
