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

On 04/04/17 11:40, Dominic Mulligan via Cl-isabelle-users wrote:
> I am running Ubuntu Linux 16.04 LTS.  There is nothing special about
> my $ISABELLE_USER_HOME as far as I can tell --- it is simply
> ~/.isabelle/Isabelle2016-1 in my home directory that was created by
> Isabelle itself.

Maybe some other persistent options change the behaviour. Can you try
with a fresh ~/.isabelle/Isabelle2016-1 directory, e.g. by renaming the
current one temporarily?

> The ~/.isabelle/Isabelle2016-1/jedit/history section does not contain
> an [isabelle-sledgehammer-provers] section at all.  It does seem to
> contain my search history within jEdit, clipboard history, and so on,
> but nothing about sledgehammer --- which is weird as I use it
> extensively.

The history file is saved by jEdit whenever the main properties have
changed and are saved, and especially on editor shutdown. You can also
invoke that operation manually in Console plugin / BeanShell:


This refers to all "history text fields" in jEdit terminology. The
Sledgehammer / Provers field is just one of them.

> The ~/.isabelle/Isabelle2016-1/etc/preferences file contains the
> key-value pair: sledgehammer_provers = "cvc4 z3 spass e
> remote_vampire" which matches what appears in the Isabelle plugin
> dialogue box within Isabelle/jEdit.  Changing the dialogue box entry,
> to include e.g. remote_spass, appears to have no effect on this
> key-value pair in ~/.isabelle/Isabelle2016-1/etc/preferences, and vice
> versa.  I assume it should?  Note that from playing around the with
> dialogue and this preferences file, I have noticed that e.g. the
> auto_nitpick key-value pair is not being updated, neither.

This is indeed very strange. You can check these Isabelle/jEdit options
in Console plugin / Scala like this:


The GUI wiring refers to the same option, see also

While we are looking at the GUI: Java/Swing look-and-feels can
occasionally play nasty tricks. How is the situation with plain-old Metal?


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