Re: [isabelle] Sledgehammer settings



Hi Joachim,

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.

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





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