Re: [isabelle] Using more provers with sledgehammer in Isabelle2016-1



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
$ISABELLE_HOME_USER directory?

The relevant information is in $ISABELLE_HOME_USER/etc/preferences and
also in $ISABELLE_HOME_USER/jedit/history (section
[isabelle-sledgehammer-provers]).


	Makarius





This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.