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?

  -- Lars





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