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
  without leading to success.

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
  a subgoal using external automatic provers. See also the
  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.