Re: [isabelle] Isabelle2013-RC1 Sledge output finicky
On 1/25/2013 2:49 PM, Makarius wrote:
In general, the ATPs are only working if they're run by themselves.
I can confirm that in both in Isabelle2012 and Isabelle2013-RC1
executing many processes in parallel on Windows/Cygwin is very
fragile. It seems to have been always like that...
As to Isabelle2012, I assume you say that because you haven't been using
Cygwin as your primary platform, but you're underselling Isabelle2012,
as far as Sledgehammer goes.
I've got most of my proofs I have now from having used Isabelle2012 with
Sledgehammer, where I was usually running a minimum of 8 ATPs on the
And that's why I isolated it down to Vampire needing to run by itself
now in Isabelle2013-RC1. With Isabelle2012, about 5 ATPs would usually
return a similar proof, but on a particular theorem, which I was running
Sledgehammer on again, there was only one good proof of about 250ms,
which I already had, but which I wasn't getting again, and I didn't know
where it had come from. I finally ran Vampire by itself to get the proof
...but only with Isabelle2012 we could speak of reasonably Windows
support in the first place. Now that so many other thinks are working
better than before, such drop-outs become more apparent.
I suppose Isabelle2012 was when Sledgehammer started being useful on
Cygwin for Sledgehammer, but with Isabelle2013, I see that the e prover
spawns about 15 processes, when it used to only start 1 or 2.
Complications are the price of progress.
Let's see if we can figure out a solution to the problem ...
Exactly. We're a team, and I'll do my share of button pushing, copying
and pasting, inserting commands, and such.
But as I so profoundly said in the past, there are no problems with
Isabelle, there are only workarounds.
For me, it would probably be running Linux under VirtualBox, which I
need to do anyway because I can only get certain local ATPs under Linux.
I'll do that after all the release candidates, unless I need to do it
I already knew that Vampire was probably the best ATP at getting proofs
for what I'm doing, but it might be better than I thought, and I might
have been missing some Vampire proofs I should have been getting with
Isabelle2012, so I'll pay more attention to that now.
However, running multiple ATPs is useful for more than just finding a
good, fast proof. Two different ATPs may return a fast proof differing
in only one proof fact, but one proof fact may be more logically
appealing than the other, such as that one is a low level theorem, and
the other is at a much higher level.
This archive was generated by a fusion of
Pipermail (Mailman edition) and