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