Re: [isabelle-dev] Sledgehammer & Nitpick "spy" mode
Am 23.09.2013 um 21:08 schrieb 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.
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
Re: [isabelle-dev] Sledgehammer & Nitpick "spy" mode
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
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
[isabelle-dev] Sledgehammer & Nitpick "spy" mode
Dear all,
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. And let me know
at some point that you have enabled the logging, so that I will remember to bug
you [*] to get the files after X months. The information stored is very crude
-- e.g. no names of theories, theorems, or constants are or will ever be
stored. It's just to get a picture of how useful (or not) these two tools are
in the wild.
Thanks for your collaboration!
Jasmin
[*] Tobias suggested calling it "prism". The recent news provide us with some
other interesting names.
[**] "bug" in the meaning of "annoy or bother" you, not "conceal a miniature
microphone", of course. ;)
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
