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 eprover.org, to motivate him to improve it further.


	Makarius





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