Re: [isabelle] Isabelle2015-RC0 available for testing
On Sun, 12 Apr 2015, C. Diekmann wrote:
* when I type sledgehammer (not using the panel), it seems as it is
only tries cvc4 and remote_vampire, is it possible to add a bit more
The Sledgehammer panel takes exactly the provers that are specified in the
input field, taking the system option "sledgehammer_provers" as default.
The 'sledgehammer' command takes a prefix of certain default provers,
depending on the nominal number of ML worker threads (which is derived
from the system option "threads").
It is up to Jasmin Blanchette to unify/simplify this further. Note that
in Isabelle2015, Sledgehammer still has various old modes stemming from
the TTY age (which has already ended).
Generally, Isabelle2015 has various changes of parallel document
processing, such that long-running print functions should no longer lead
to exhaustion of worker threads as before. This should improve the degree
of parallelism with the Sledgehammer panel vs. ongoing edits. If there are
remaining problems with it, the coming weeks of Isabelle2015-RC testing
are an opportunity to report them.
This archive was generated by a fusion of
Pipermail (Mailman edition) and