[isabelle-dev] PG preferences (auto solve in particular)
makarius at sketis.net
Wed Nov 11 10:52:24 CET 2009
On Wed, 11 Nov 2009, Florian Haftmann wrote:
> I'm currently asking myself whether the substructure of Isabelle
> settings in the preferences menu is already carved in stone (although
> only some adventurous people seem to be using PG 4 by now).
> In my naive view the distinction between "Display" and "Advanced
> display" is quite artifical, whereas things like "Auto solve" and "Auto
> nitpick" should be better placed in a separate menu "Hints". Or is
> there a rationale I am not aware of for the current categorization?
Without consulting the Mercurial history, I would say these categories
were introduced by David Aspinall together with the first version of the
formalized preferences concept (which is the only part of the Isabelle
PGIP implementation that was ever used widely).
Before PG 4 the grouping of prefs is not directly reflected in the menus,
so nobody noticed potential oddities.
Anyway, my may concern about PG 4 is to see it working at all. There are
many fundamental problems remaining. Only two days ago I've found myself
doing proofs with isabelle tty, because there was a Spontaneous Massive
Existence Failure of PG 3.7.1 and PG pre-4 on Ubuntu 9.10, concerning
Emacs 22 and 23 (Gtk). (Those who are not following the Ubuntu or PG
issue tracker, can use plain old emacs22-x until things are sorted out.)
IIRC, you are also using Ubuntu 9.10. Which version of Emacs works for
More information about the isabelle-dev