Re: [isabelle] provers used by sledgehammer



Am 20.07.2012 um 09:37 schrieb Lars Noschinski:

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

Yes, but then why not do it for Nitpick, Quickcheck, Refute? And what about other options, e.g. simplifier traces? Whatever we do, it's going to be tedious, inconsistent, or both.

Jasmin






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