[isabelle-dev] Sledgehammer on Cygwin

[Makarius]

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