Email Gateway (Aug 22 2022 at 13:13): Email Gateway (Aug 22 2022 at 13:13):From: Christoph Dittmann <f-isabellelist@yozora.eu>
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
Email Gateway (Aug 22 2022 at 13:13):From: Jasmin Blanchette <jasmin.blanchette@inria.fr>
Hi Christoph,
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
This is because the "smart" default list of provers is used, and that smart default does just that. Write
sledgehammer_params
to see the default (under "provers =").
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
I presume you are referring to the Sledgehammer panel. The panel has its own options and lives its own life. These options only concern the "Apply" button in the panel, not the lower-level "sledgehammer" (and "sledgehammer_param") commands.
I hope this clarifies things.
Cheers,
Jasmin
Last updated: Apr 19 2024 at 04:17 UTC