[isabelle-dev] Sledgehammer on Cygwin

Makarius makarius at sketis.net
Tue Apr 24 17:21:00 CEST 2012

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:

line 24: 
Permission denied
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.


More information about the isabelle-dev mailing list