Email Gateway (Aug 22 2022 at 15:14): Email Gateway (Aug 22 2022 at 15:14):From: Dominic Mulligan via Cl-isabelle-users <cl-isabelle-users@lists.cam.ac.uk>
Hi,
I'm trying to use some more of the remote provers with sledgehammer in
Isabelle2016-1, but seem to be having trouble getting sledgehammer to
pay any attention to my changes in the Plugins>Plugin
options>Isabelle>General dialog box.
In particular, it seems that the default value in the Sledgehammer
Provers field in that dialog box is hardcoded, in that any changes to
the default value of "cvc4 z3 spass e remote_vampire" are ignored by
Isabelle. Expanding this field to e.g. "cvc4 z3 spass e
remote_vampire remote_e remote_waldmeister" has no effect whatsoever
on sledgehammer's execution.
Note also, in normal operation, despite the default value of that
field, sledgehammer never seems to invoke remote_vampire, instead only
invoking cvc4, spass, e, and z3.
Further, modifying the contents of
$ISABELLE_HOME/src/HOL/Tools/etc/options does seem to have an effect,
in that the tooltip you obtain when hovering over the Sledgehammer
Provers field reflects the contents of that file (the field itself
does not change), but again does not seem to have any effect on
sledgehammer's execution.
Note that manually setting the sledgehammer prover options at the
point of invocation does work, as in:
sledgehammer[provers="cvc4 z3 spass e remote_vampire remote_e
remote_waldmeister remote_iprover remote_snark"]
correctly invokes all listed theorem provers on a problem. However, I
would like to be able to set this option globally, rather than having
to type out a massive string at every use of sledgehammer.
Is there a way around this problem? (I first noticed the problem in
Isabelle-2016, before trying to upgrade to Isabelle2016-1 this
morning, where it persists).
Thanks,
Dominic
Last updated: Apr 25 2024 at 20:15 UTC