[isabelle-dev] Sledgehammer

[Jasmin Christian Blanchette]

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