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.blanche...@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
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
