On Mon, 23 Apr 2012, Makarius wrote:
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.
There are still various open questions here.
The "Internal error ..." might be a hard crash of the external bash
process. I can't say at the moment where the Empty exception is from, and
if it is Jasmin or myself who could make the error more informative.
The underlying physical problem is from Cygwin, which sometimes needs
magic incantations like this to do well (from Windows cmd.exe):
...\contrib\cygwin-1.7.9\bin\ash -c /bin/rebaseall
I will try to build this maintenance thing into the monolithic
application.
Having Cygwin in proper shape again, I can confirm that sleghammer does
work in many situations, but not all:
theory A imports Main begin
lemma "[a] = [b] ==> a = b" sledgehammer [provers = e]
Sledgehammer: "e" on goal
[a] = [b] ==> a = b
"e": The prover ran out of resources.
Any clues? How can one get more information from the external prover?
Makarius
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
