Re: [isabelle] 5 proofs of concept satisfied and awesomeness revisited

On Thu, 12 Jul 2012, Gottfried Barrow wrote:

What you should know is that with Isabelle2011-1, sledgehammer running under Cygwin was useless. It wouldn't ever come back, or it would timeout. I knew sledgehammer worked because I tried it out under Linux.

I tried sledgehammer, not expecting any results. I got results. In particular, the structured proof stood out because it's not a one-line statement telling you, "Found proof".

Two screen shots are attached. One shows the structured proof that it found that it doesn't find anymore. I assume it's because CPU resources got sucked up by Windows for something else. I'll try setting the options later.

There is indeed a big difference of sledgehammer in Isabelle2011-1 vs. Isabelle2012. The current release might still have some drop-outs, though. If you spot anything specific, keep telling us (either the mailing list, or Jasmin Blanchette, or me).

In particular, I suspect that E prover 1.4/1.5 still has too much shell scripting built-in to work smoothly on Cygwin. It might also help to point out such observations to Stephan Schulz from, to motivate him to improve it further.


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