Email Gateway (Aug 19 2022 at 12:49): Email Gateway (Aug 19 2022 at 12:49):From: Joachim Breitner <breitner@kit.edu>
Hi,
I noticed that the sledgehammer timeout can be configured in the
Isabelle plugin settings of jEdit. I would appreciate if I could also
configure the set of default solvers there, so that it would apply to
both “sledgehammer” entered by hand, and the sledgehammer panel.
Until then: What file do I have to modify how to configure it manually?
Thanks,
Joachim
signature.asc
Email Gateway (Aug 19 2022 at 12:49):From: Jasmin Blanchette <jasmin.blanchette@gmail.com>
Hi Joachim,
Am 08.11.2013 um 11:10 schrieb Joachim Breitner <breitner@kit.edu>:
I noticed that the sledgehammer timeout can be configured in the
Isabelle plugin settings of jEdit. I would appreciate if I could also
configure the set of default solvers there, so that it would apply to
both “sledgehammer” entered by hand, and the sledgehammer panel.
That would be nice indeed. Technically it's a bit tricky right now, because unlike for timeouts the default set of solver depends on how many cores you have and which provers are installed (which may change over time). Perhaps Makarius can comment on how feasible such an option is.
As an alternative, if all your theories import the same base theory, say Base.thy, you can put
sledgehammer_params [provers = e z3 yices etc]
in there.
Until then: What file do I have to modify how to configure it manually?
If you're talking about editing Isabelle source, the absolute simplest way would be to add a command
sledgehammer_params [provers = e z3 yices etc]
to "src/HOL/Main.thy" (which you presumably import). If you're a glutton for punishment, you could also edit "src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML" and tamper with the aptly named function "default_provers_param_value".
I hope this helps.
Regards,
Jasmin
Email Gateway (Aug 19 2022 at 12:51):From: Makarius <makarius@sketis.net>
On Fri, 8 Nov 2013, Jasmin Blanchette wrote:
Am 08.11.2013 um 11:10 schrieb Joachim Breitner <breitner@kit.edu>:
I noticed that the sledgehammer timeout can be configured in the
Isabelle plugin settings of jEdit. I would appreciate if I could also
configure the set of default solvers there, so that it would apply to
both “sledgehammer” entered by hand, and the sledgehammer panel.
Invoking sledgehammer by hand introduces an extra dimension of
complication. What are the remaining reasons to do so?
That would be nice indeed. Technically it's a bit tricky right now,
because unlike for timeouts the default set of solver depends on how
many cores you have and which provers are installed (which may change
over time). Perhaps Makarius can comment on how feasible such an option
is.
Event though I made some protocol to pass sledgehammer params from
Isabelle/ML to Isabelle/Scala in certain situations, I don't understand
all the possibile sources of options. In the next round we should try
hard to make it as simple as possible, but not simpler.
For example, assuming that the Sledgehammer panel is used by default ---
anything else only in extraordinary situations --- the panel could just
provide access to some clickable "dashboard" of provers. No magic
defaults, just plain persistence of user-provided options in some way or
the other.
Makarius
Email Gateway (Aug 19 2022 at 12:51):From: Joachim Breitner <breitner@kit.edu>
Hi,
changing a now failing
by (metis a b c d e )
to
sledgehammer (add: a b c d e)
which is often faster running sledgehammer without hints
visual feedback in the document about where sledgehammer is running
(as far as I could tell, the sledgehammer panel does not leave a
mark in the document, e.g. a spinner of some kind, which would be
useful visual feedback).
and of course: habit ;-)
Greetings,
Joachim
signature.asc
Email Gateway (Aug 19 2022 at 12:53):From: Gottfried Barrow <gottfried.barrow@gmx.com>
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
Email Gateway (Aug 19 2022 at 12:53):From: Makarius <makarius@sketis.net>
That is not inherent in the separate command vs. panel. It is merely
accidental which options are available where.
At some point I need to discuss with Jasmin to sort out what really needs
to be supported in the panel, such that a manual invocation of the
sledgehammer command becomes a rare event.
Makarius
Last updated: May 06 2024 at 16:21 UTC