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

Re: [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

___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev