[isabelle] Isabelle2016: sledgehammer ignores prover list
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
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"?
This archive was generated by a fusion of
Pipermail (Mailman edition) and