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
[email protected]
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
