[isabelle-dev] Sledgehammer & Nitpick "spy" mode

[Makarius]

On Mon, 23 Sep 2013, Jasmin Christian Blanchette wrote:

> Starting with Isabelle/58d1b63bea81, Sledgehammer and Nitpick have a 
> "spy" mode [*] that log all invocations to those two tools in 
> "~/.isabelle/spy_{sledgehammer,nitpick}". If you are willing to be part 
> of a big experience in the name of science, please add
>
>    SLEDGEHAMMER_SPY=yes
>    NITPICK_SPY=yes
>
> to your "~/.isabelle/etc/settings" file to enable the logging.

Just a technical note: it is now quite easy to make persistent Isabelle 
system options with GUI access in Isabelle/jEdit (even Proof General).
Then users no longer have to edit etc/settings files and reboot the 
system.

See for example Isabelle/e18a028b345c where this is done for 
sledgehammer_timeout.  The canonical access from Isabelle/ML is via 
Options.default_int @{option sledgehammer_timeout}.

The position within Isabelle/jEdit plugin options is determined by the 
"section" and the "public" flag of the etc/options entry.  Right now, 
"Miscellaneous Tools" is the one section for any such HOL tools.  (I am 
still considering to make Z3_NON_COMMERCIAL an Isabelle system option like 
this for the coming release, although I got distracted with too many other 
things, and users of tools by Microsoft might actually expect a 
requirement to reboot after change of configuration :-).


 	Makarius