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 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


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