Email Gateway (Aug 18 2022 at 20:02): Email Gateway (Aug 18 2022 at 20:02):From: Makarius <makarius@sketis.net>
Dear Isabelle users,
official Isabelle2012 will be rolled-out before the end of the month.
Release candidate #1 is now available here:
http://isabelle.in.tum.de/website-Isabelle2012-RC1
Some parts of the website are not finished yet, notably the announcement
with list of main novelties, but NEWS is already in shape -- with a bit
more than 1000 lines of user-relevant changes.
From the system-integration standpoint there are the following main
improvements:
* Smart download button right on the front-page (please tell if it does
not work on your browser and your operating system).
* Self-extracting archive for Windows (all-inclusive at 770 MB)
* Z3 for Mac OS (thanks to MSR)
Please try it on your machine, and report any problems either on the
mailing list or to me personally.
Makarius
Email Gateway (Aug 18 2022 at 20:03):From: Jasmin Blanchette <jasmin.blanchette@gmail.com>
Hi Makarius,
official Isabelle2012 will be rolled-out before the end of the month. Release candidate #1 is now available here:
http://isabelle.in.tum.de/website-Isabelle2012-RC1
Some parts of the website are not finished yet, notably the announcement with list of main novelties, but NEWS is already in shape -- with a bit more than 1000 lines of user-relevant changes.
[...]
Please try it on your machine, and report any problems either on the mailing list or to me personally.
I tried Nitpick and Sledgehammer on Mac OS X 10.6 and a Windows XP VirtualBox. On Mac OS X, everything went with both PIDE and PG. The only slightly strange thing I noticed is that one needs to click the "Update" button explicitly to get the right output for "ML {* ... *}" commands.
On Win XP, I first got the error: "Failed to start Isabelle process". The error message started with "perl 3396! _pinfo::dup_proc_pipe: DuplicateHandle failed". The second time around it worked, but when I tried Sledgehammer on a very easy goal E just timed out. Sometimes clicking the Isabelle icon pops up the Isabelle splash screen and then just silently dies. All these issues appear to be due to some low-level system failure, probably related to the little resources allocated to that VirtualBox installation.
For the record: I tried with "overlord" on; then the first line in "~/.isabelle/Isabelle2012-RC1/prob_e_1" gives the exact command line. I copy pasted it into a Cygwin terminal and it worked perfectly well (i.e. E output a proof ending with "SZS output end CNFRefutation").
I hope somebody else with a (perhaps more modern) Windows installation can check whether E works. The simple property I tried is
lemma "hd [a] = hd [b] ==> a = b"
sledgehammer
and a proof should be found very quickly by all available provers (E, SPASS, remote Vampire, remote E-SInE).
Jasmin
Email Gateway (Aug 18 2022 at 20:03):From: Makarius <makarius@sketis.net>
Maybe it just takes very long to startup. There are two stages:
* "Isabelle" splash: the .exe wrapper is starting up a JVM with
isabelle.Main class
* "jEdit" splash: jEdit is starting up within the usual Isabelle
environment
There is a timeout on the "Isabelle" splash, so it might disappear before
the rest is coming up.
It is also possible to open the Cygwin-Terminal and run "isabelle jedit",
which might show errors better, although the Java based startup should
display errors as well (hopefully).
Makarius
Email Gateway (Aug 18 2022 at 20:03):From: Makarius <makarius@sketis.net>
I have seen the E timeout before, but could not pin it down yet. Running
with overlord, I see that it starts relatively ambitious shell scripts by
Stephan Schulz. Cygwin is a bit slow at that, especially when several
such shell scripts are run in parallel.
Is there a way to restrict Slegehammer ATPs to 1 parallel instant?
This would help to test this hypothesis.
Makarius
Email Gateway (Aug 18 2022 at 20:04):From: Jasmin Blanchette <jasmin.blanchette@gmail.com>
Indeed, if I give it enough time, that's what happens.
Jasmin
Email Gateway (Aug 18 2022 at 20:04):From: Jasmin Blanchette <jasmin.blanchette@gmail.com>
If you run
sledgehammer [provers = e]
you'll get only one prover and hence only one active thread.
Jasmin
Last updated: Apr 26 2024 at 12:28 UTC