Re: [isabelle] Sledgehammer settings



On 11/11/2013 4:52 AM, Makarius wrote:
Invoking sledgehammer by hand introduces an extra dimension of complication. What are the remaining reasons to do so?

To be able to change the default options.

I use "preplay_timeout=10" and "verbose=true", which can't be changed in the "Plugin Options/Isabelle/General". By using "verbose=true", I learned to use "preplay_timeout=10".

I don't like getting results that say something like "try this...", with a minimize command and 20 facts as part of it, because in the past, I would click on those, Sledgehammer would replay the proof, the 20 facts wouldn't get minimized, and the proof would be slow, or not terminate after many seconds. I don't want to do that 6 times for 6 proofs that may get found like that.

So, I set "preplay_timeout=10", where the default is "preplay_timeout=3", and I normally don't try any proof which Sledgehammer hasn't replayed back to eliminate all unneeded facts. If I'm desperate, I may do things different.

I learned this from using "verbose=true". I would see Sledgehammer replaying a proof, and eliminating facts, but then it would timeout, because there were lots of facts it needed to try and eliminate, and "preplay_timeout=3" was too short.

I don't change my Sledgehammer options much now, but by watching the output, I may see something that helps me automate Sledgehammer better for my needs.

The Sledgehammer panel is convenient, but, say, 50% of the time, for a new theorem, I'm not going to get a proof. I will then want to run it again, by inserting the command "sledgehammer" in the file with "verbose=true", to see if I get any information from Sledgehammer that will help me. Rather than run Sledgehammer twice 50% of the time, I'd rather always use my own command 100% of the time to prevent that.

Occasionally, I'll even learn something from just looking at the long list of facts it starts with, or that it's only found 5 facts applicable, when it normally uses hundreds.

Regards,
GB






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