Re: [isabelle-dev] Isabelle release test website
On Tue, 24 Apr 2012, Jasmin Christian Blanchette wrote: Am 23.04.2012 um 17:22 schrieb Makarius: Here is an update of the test website for warming up a bit more http://www4.in.tum.de/~wenzelm/test/website/ I've spent this cold and wet weekend to produce a monolitic Windows application, which bundles both JDK and Cygwin 1.7.9, see the Download page. (Cygwin 1.7.9 is important here, because in the later version from this year Poly/ML multithreading is a bit unstable.) I use Windows XP on VirtualBox. I downloaded the Isabelle_23-Apr-2012.exe file, moved it to my home directory. Then I started Isabelle.exe and waited over a minute but nothing happened. I suppose here that the self-extracting Isabelle_23-Apr-2012.exe archive did extract correctly, to something like 850 MB directory structure? Then I tried ./bin/isabelle tty but got the message 'Unknown logic HOL -- no heap file found in: /cygdrive/c/.../heaps/polyml-undefined_x86-cygwin Could it be due to Cygwin somehow? I don't know how to launch a terminal for Cygwin 1.7.9, so I'm still using the old terminal for whatever version of Cygwin I had on the machine already. Your existing Cygwin is probably relatively old, such that the poly.exe cannot be started and produce the required version; cf. the undefined above. Starting a terminal for the bundled Isabelle Cygwin now works, but I did not update the 7zip SFX yet. You can do it via http://www4.in.tum.de/~wenzelm/test/website/dist/Isabelle_23-Apr-2012_bundle_x86-cygwin.tar.gz by untarring that with the existing Cygwin. Then the directory structure can be access via Windows the standard way. There are now Cygwin-Terminal and Cygwin-Setup batch files to be clicked on, which hopefully do the job. You might still have to do a manual incantation from cmd.exe: ...\contrib\cygwin-1.7.9\bin\ash -c /bin/rebaseall This maintenance step requires all Cygwin stuff to be off. 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
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
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] Isabelle release test website
Hi Makarius, I suppose here that the self-extracting Isabelle_23-Apr-2012.exe archive did extract correctly, to something like 850 MB directory structure? At least it had the expected directory structure. Your existing Cygwin is probably relatively old, such that the poly.exe cannot be started and produce the required version; cf. the undefined above. Indeed, that must have been it. Starting a terminal for the bundled Isabelle Cygwin now works, but I did not update the 7zip SFX yet. You can do it via http://www4.in.tum.de/~wenzelm/test/website/dist/Isabelle_23-Apr-2012_bundle_x86-cygwin.tar.gz by untarring that with the existing Cygwin. Then the directory structure can be access via Windows the standard way. There are now Cygwin-Terminal and Cygwin-Setup batch files to be clicked on, which hopefully do the job. That works. Thanks! And indeed, I can reproduce Alex's issue. You might still have to do a manual incantation from cmd.exe: ...\contrib\cygwin-1.7.9\bin\ash -c /bin/rebaseall This maintenance step requires all Cygwin stuff to be off. That didn't seem to be necessary. Jasmin ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] spass: Internal error: exception Empty raised (line 458 of library.ML)
On Tue, 24 Apr 2012, Jasmin Christian Blanchette wrote: Am 23.04.2012 um 22:02 schrieb Makarius: On Mon, 23 Apr 2012, Alexander Krauss wrote: Sledgehammering... spass: Internal error: exception Empty raised (line 458 of library.ML) 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. I can reproduce it on my WinXP-on-VirtualBox installation. There are a couple of variants of this: Sometimes it affects a remote prover, sometimes I get an empty string error from remote_e. It's certainly not tied to spass. The error seems to go away when an explicit prover is specified by passing [prover = ...] to the sledgehammer command. I'll see if I can debug this further. I can't seem to get this to happen with the Mac bundle (from 23 April 2012). I have also made some more experiments. The Empty exception is from the split_last here http://isabelle.in.tum.de/repos/isabelle/file/ea153f6abdb6/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML#l614 where you don't get any output unexpectedly, bacause /bin/sh has crashed. Ouch! Such things happen on Cygwin. I will try to sort out the physical problem. Maybe you can make the ML part more informative nonetheless. Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] spass: Internal error: exception Empty raised (line 458 of library.ML)
Am 24.04.2012 um 20:27 schrieb Jasmin Christian Blanchette: I can reproduce it on my WinXP-on-VirtualBox installation. There are a couple of variants of this: Sometimes it affects a remote prover, sometimes I get an empty string error from remote_e. It's certainly not tied to spass. The error seems to go away when an explicit prover is specified by passing [prover = ...] to the sledgehammer command. Update: I couldn't track it down with 100% certainty, but I strongly suspect that the Empty exception stems from the split_last call in sledgehammer_provers.ML, which extracts the timing value output by the Unix time command. There's an assumption lurking in there that the output of time foobar will be at least one line long, which seems reasonable but appears to be violated by Isabelle on Cygwin once every so often. There appears to be something fishy going on with parallel bash_output calls. In any case, I've now made the code more robust to at least avoid the exception (change 63c939dcd055). Jasmin ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] spass: Internal error: exception Empty raised (line 458 of library.ML)
Am 24.04.2012 um 20:58 schrieb Makarius: have also made some more experiments. The Empty exception is from the split_last here http://isabelle.in.tum.de/repos/isabelle/file/ea153f6abdb6/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML#l614 where you don't get any output unexpectedly, bacause /bin/sh has crashed. Ouch! Such things happen on Cygwin. I will try to sort out the physical problem. Maybe you can make the ML part more informative nonetheless. OK, it looks like we came to the same conclusion (see my email from one minute ago). Jasmin ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
