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
Stay tuned ...
This archive was generated by a fusion of
Pipermail (Mailman edition) and