Am 23.09.2013 um 21:08 schrieb Makarius <makar...@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
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
