[isabelle-dev] Sledgehammer on Cygwin

[Jasmin Blanchette]

Am 24.04.2012 um 17:21 schrieb Makarius:

> 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.

Yes; it's based on the E message "# Cannot determine problem status within resource limit", which is also wrong... I'll remove it.

I've updated the "e-1.4.tgz" package on my website so that it has +x for all three ".exe" files.

Jasmin