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"
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.
This archive was generated by a fusion of
Pipermail (Mailman edition) and