Email Gateway (Mar 13 2023 at 16:28): Email Gateway (Mar 13 2023 at 16:28):From: Dominic Mulligan <cl-isabelle-users@lists.cam.ac.uk>
Hi,
Is there a graceful way to ensure that Isabelle does not transmit anything
to the SystemOnTPTP service when executing Sledgehammer? Removing the URL
in the Plugin Settings pane in Isabelle/jEdit seems to work but this also
floods the Sledgehammer output pane with warnings about malformed URLs.
Thanks,
Dominic
Email Gateway (Mar 13 2023 at 16:50):From: Jasmin Blanchette <jasmin.blanchette@ifi.lmu.de>
Dear Dominic,
I can only think of one way: You can set the provers using "sledgehammer_params [provers = xxx]", where "xxx" is the list of provers you want to run (e.g. "e spass vampire zipperposition cvc4 verit z3"). This you could do once and for all in a base theory you import from everywhere else. If you use the Sledgehammer panel, you might have to enter the list of provers there manually instead.
(In the repository version of Isabelle, we have already disabled SystemOnTPTP by default, so the issue should be gone in the next release.)
Best,
Jasmin
Email Gateway (Mar 13 2023 at 19:07):From: Dominic Mulligan <cl-isabelle-users@lists.cam.ac.uk>
Great, thanks for that tip!
Last updated: Apr 23 2024 at 20:15 UTC