[isabelle] Isabelle2016: sledgehammer ignores prover list



Hi,

when I write "sledgehammer" in the main Isabelle/jEdit window in
Isabelle2016, the "output" panel shows a list of sledgehammer results,
as expected.  However, it
1) lists at most as many results as the "threads" configuration says,
   so 4 threads = 4 results
2) seems to ignore the list of provers I give to sledgehammer in the
   Isabelle plugin configuration.

For example, the default list of provers is:
  e z3 cvc4 spass remote_vampire

In the sledgehammer panel, everything works fine and it runs all of the
provers.

With 4 threads, the output panel only shows the results of e, z3, cvc4
and spass.  With 6 threads, it additionally shows the results of vampire
and of remote_e_sine, which are not in the list of provers at all.

What am I doing wrong?  How can I convince sledgehammer to respect the
list of provers when I start it by typing "sledgehammer"?

Best,
Christoph




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