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.


	Makarius





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