# Re: [isabelle] RC4: sledgehammer on Cygwin crashed once; temp file not removed

On Tue, 26 Aug 2014, Gottfried Barrow wrote:


"Auto Methods", mysteriously, could also be putting demands on the CPU when Sledgehammer is running.

This is what the Isabelle/jEdit manual says in Isabelle2014:

\item @{system_option_ref auto_methods} controls automatic use of a
combination of standard proof methods (@{method auto}, @{method
simp}, @{method blast}, etc.).  This corresponds to the Isar command
@{command_ref "try0"} \cite{isabelle-isar-ref}.

The tool is disabled by default, since unparameterized invocation of
standard proof methods often consumes substantial CPU resources


There might be additional reasons for its CPU hunger. If so, I can refine the text accordingly.



"Auto Solve direct" seems to not be a problem, because I've left it enabled, and I don't use "Auto Sledgehammer".

More quotes from the manual:

\item @{system_option_ref auto_sledgehammer} controls a significantly
reduced version of @{command_ref sledgehammer}, which attempts to prove
Sledgehammer manual \cite{isabelle-sledgehammer}.

This tool is disabled by default, due to the relatively heavy nature
of Sledgehammer.

\item @{system_option_ref auto_solve_direct} controls automatic use of
@{command_ref solve_direct}, which checks whether the current subgoals
can be solved directly by an existing theorem.  This also helps to
detect duplicate lemmas.

This tool is \emph{enabled} by default.


The CPU goes to about 50% as shown for all four cores, and then I have to terminate. Disabling the three options is not enough.


You can also experiment with the improved Monitor panel, to get some statistics of the running ML system from inside.


Makarius



This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.