Re: [isabelle] Using more provers with sledgehammer in Isabelle2016-1
- To: Dominic Mulligan <dominic.p.mulligan at googlemail.com>, cl-isabelle-users at lists.cam.ac.uk
- Subject: Re: [isabelle] Using more provers with sledgehammer in Isabelle2016-1
- From: Makarius <makarius at sketis.net>
- Date: Sun, 2 Apr 2017 19:53:56 +0200
- In-reply-to: <CAFAp4Fk0pG50upsy53BN3e2V5qH_sJhfn2Lx7nhbqme9EoWNHg@mail.gmail.com>
- References: <CAFAp4Fk0pG50upsy53BN3e2V5qH_sJhfn2Lx7nhbqme9EoWNHg@mail.gmail.com>
- User-agent: Mozilla/5.0 (X11; Linux x86_64; rv:45.0) Gecko/20100101 Thunderbird/45.8.0
On 02/03/17 11:07, Dominic Mulligan via Cl-isabelle-users wrote:
> 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.
This is very strange. I've just tried it in Isabelle2016 and
Isabelle2016-1 and it works as expected (on Linux).
Note that the text field labeled "Provers:" and the Isabelle plugin
option value "sledgehammer_provers" are shared. This means changing one
also changes the other (persistently).
What is your OS platform? Do you have anything special concerning your
The relevant information is in $ISABELLE_HOME_USER/etc/preferences and
also in $ISABELLE_HOME_USER/jedit/history (section
This archive was generated by a fusion of
Pipermail (Mailman edition) and