Re: [isabelle] Isabelle2012-RC1 available for testing



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






This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.