Re: [isabelle] Sledgehammer settings
On Fri, 8 Nov 2013, Jasmin Blanchette wrote:
Am 08.11.2013 um 11:10 schrieb Joachim Breitner <breitner at 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
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
This archive was generated by a fusion of
Pipermail (Mailman edition) and