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