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

[Jasmin Blanchette]

Am 23.09.2013 um 21:08 schrieb Makarius <makarius at sketis.net>:

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

Good point. This "spy" mode does feel like somewhat of a low-level hack that perhaps shouldn't be exposed too prominently, but even then perhaps there would be no harm in making them real options. I'll sleep on it.

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

Indeed, that would be nice. :) But there's always a next release.

Jasmin