Re: [isabelle] provers used by sledgehammer
On 20.07.2012 09:19, Jasmin Blanchette wrote:
Am 20.07.2012 um 04:46 schrieb Christian Sternagel:
it seems that "just" spass, e, remote_vampire, remote_e_sine, and z3 are run; but not yices. Can I change this globally (e.g., in my etc/settings) without having to use sledgehammer_params or explicitly setting options when calling sledgehammer?
If you change it through the good old Proof General settings, I think it will do the right thing and remember it across sessions. Otherwise, no: That's what "sledgehammer_params" is for, and it would be tedious to emulate its functionality in "etc/settings" (e.g. to change the default timeout or whatever else...).
I'm fine with the default settings, so I don't have a need for this
functionality; but could you not just reuse the parser for
sledgehammer_params to parse a $SLEDGEHAMMER_PARAMS environment
variable, when you setup the default values?
This archive was generated by a fusion of
Pipermail (Mailman edition) and