[isabelle-dev] Sledgehammer on Cygwin

[Makarius]

On Tue, 24 Apr 2012, Jasmin Christian Blanchette wrote:

> To get even more information, you can even pass "overlord" (sic):
>
>   sledgehammer [provers = e, debug, overlord]
>
> Then you get files called "prob_e_1" (E's input) and "prob_e_1_proof" 
> (E's output) in your "~/.isabelle" directory. This is very 
> thread-unsafe, but I find it extremely useful for debugging.

I did not dare to enable overlord mode so far, but doing it on your 
behalf it reveals the follow in prob_e_1_proof:

/cygdrive/c/Users/wenzelm/Desktop/Isabelle_23-Apr-2012/contrib/e-1.4/x86-cygwin/eproof: 
line 24: 
/cygdrive/c/Users/wenzelm/Desktop/Isabelle_23-Apr-2012/contrib/e-1.4/x86-cygwin/eprover: 
Permission denied
sh: 
/cygdrive/c/Users/wenzelm/Desktop/Isabelle_23-Apr-2012/contrib/e-1.4/x86-cygwin/eprover: 
Permission denied
# Cannot determine problem status within resource limit


Which means you merely need to give extra chmod +x for the .exe files in 
your component tar.gz.  Windows does not require that, but Cygwin.

Nonetheless, the error message about resources is a bit odd.


 	Makarius