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
