Re: [isabelle] provers used by sledgehammer



On Fri, 20 Jul 2012, Jasmin Blanchette wrote:

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.

That would indeed stretch the Isabelle system settings concept a bit far. There are also physical limitations on the process environment size, notably on Windows.

No need to worry about the above problems, though. At the next stage, the Isabelle/Scala infrastructure will provide a concept of externalized options, somehow in correspondence to internal configuration options, with some support to make them persistent as preferences. So the tendency will be to declare such options once and for all, and let the user modify them either within the theory context, or as background default for the running session.

Stay tuned ...


	Makarius






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