[isabelle-dev] Sledgehammer

[Clemens Ballarin]

Hi Jasmin,

Thanks for this hint.  It turns out that I had set E_HOME to some  
bogus location.  Residue of some old setup...  Now it work fine.

Clemens


Quoting Jasmin Christian Blanchette <jasmin.blanchette at gmail.com>:

> Am 24.06.2011 um 20:13 schrieb Clemens Ballarin:
>
>> While doing an 'isabelle makeall all' on my local machine, I  
>> encountered the error
>>
>>  Sledgehammering...
>>  *** Unexpected outcome: "unknown".
>>  *** At command "sledgehammer" (line 26 of  
>> "/Users/ballarin/isabelle/hg/src/HOL/Metis_Examples/Proxies.thy")
>>
>>
>> I guess I lack some sort of heavy equipment here.  What surprises  
>> me is that on macbroy2 I don't have set up sledgehammer either, but  
>> I don't get this error.
>
> These tests have a test to check whether you have the necessary  
> equipment, so this is strange. Could you tell me what
>
>     ML {* getenv "E_HOME" *}
>
> outputs on this installation and if it's not the empty string check  
> whether there's an executable "eproof" script in that directory.  
> Also, what happens if you write
>
>     lemma "x = y ==> y = x"
>     sledgehammer [e, verbose]
>
> ?
>
> Thanks,
>
> Jasmin
>