Re: [isabelle] auto sledgehammer? [Re: 2013-1-RC1: proof method suggested try or try0 no longer overwrites 'try' keyword]



Hi Christoph,

> Thanks for pointing out!  Very interesting to know, but (now take this
> as feedback from a naive end-user) I probably won't enable all these
> automations seems.  Auto quickcheck and solve_direct are very nice, but
> I wouldn't want time-consuming tools (such as Sledgehammer) to run
> automatically even while I am still editing a statement.  I made it into
> a habit to invoke "try" whenever I've finished writing down a statement.

Auto Sledgehammer and Auto Nitpick run in a much reduced mode -- e.g. Sledgehammer just tries one prover for a few seconds instead of four for half a minute. (The manuals of these tools clarify which options are used.)  I've enabled them months ago and don't really notice them any more than I notice Auto Quickcheck or Auto solve_direct. On the other hand, if you invoke "try" regularly, I can see that you don't need those tools.

Regards,

Jasmin





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