[isabelle-dev] Sledgehammer on Cygwin
makarius at sketis.net
Tue Apr 24 14:52:06 CEST 2012
On Mon, 23 Apr 2012, Makarius wrote:
> On Mon, 23 Apr 2012, Alexander Krauss wrote:
>> "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
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
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?
More information about the isabelle-dev