Re: [isabelle] Isabelle2012-RC1 available for testing



On Fri, 4 May 2012, Jasmin Blanchette wrote:

The second time around it worked, but when I tried Sledgehammer on a very easy goal E just timed out.

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).

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





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