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 first attempt.

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

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

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.

Regards,
GB






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