Re: [isabelle-dev] Sledgehammer on Cygwin
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
Re: [isabelle-dev] Sledgehammer on Cygwin
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
Hi Makarius, > There are still various open questions here. I will look into this later today. > lemma "[a] = [b] ==> a = b" sledgehammer [provers = e] > > Sledgehammer: "e" on goal > [a] = [b] ==> a = b > > "e": The prover ran out of resources. > > Any clues? How can one get more information from the external prover? sledgehammer [provers = e, verbose] or the strictly more verbose sledgehammer [provers = e, debug] often help. 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. But it's on my radar. I tested the 23 April package's Sledgehammer on my Mac (Snow Leopard) this morning and it worked like a charm. I'll try to reproduce the issues on Cygwin now when I get a second. Jasmin ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
[isabelle-dev] Sledgehammer on Cygwin
On Mon, 23 Apr 2012, Makarius wrote: On Mon, 23 Apr 2012, Alexander Krauss wrote: Sledgehammering... "spass": Internal error: exception Empty raised (line 458 of "library.ML") "remote_vampire": Try this: by metis (12 ms). "remote_e_sine": Try this: by metis (13 ms). I've seen it before, but for the remote provers, and did not investigate further yet. My first idea was it could be a problem of the network connection of the heavily fortified vmbroy9 machine, but spass is certainly local. There are still various open questions here. The "Internal error ..." might be a hard crash of the external bash process. I can't say at the moment where the Empty exception is from, and if it is Jasmin or myself who could make the error more informative. The underlying physical problem is from Cygwin, which sometimes needs magic incantations like this to do well (from Windows cmd.exe): ...\contrib\cygwin-1.7.9\bin\ash -c /bin/rebaseall I will try to build this maintenance thing into the monolithic application. Having Cygwin in proper shape again, I can confirm that sleghammer does work in many situations, but not all: theory A imports Main begin lemma "[a] = [b] ==> a = b" sledgehammer [provers = e] Sledgehammer: "e" on goal [a] = [b] ==> a = b "e": The prover ran out of resources. Any clues? How can one get more information from the external prover? Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
