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

Makarius makarius at sketis.net
Mon Sep 23 21:08:47 CEST 2013

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

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 :-).


More information about the isabelle-dev mailing list