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