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

[Jasmin Christian Blanchette]

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