[isabelle-dev] PG preferences (auto solve in particular)

[David Aspinall]

> 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).

I think when I added the categories there were no settings for automated 
assistance at all, which is I guess why people who added them later put 
them under Tracing.  You could easily introduce a new category instead.

Nothing is set in stone as far as PG is concerned, although the 
categories do appear in the names of the customized variables used by 
"Save Settings" so people may lose their settings if names or categories 
change.

> Anyway, my may concern about PG 4 is to see it working at all.  There 
> are many fundamental problems remaining.  

I only know of what's on trac, http://proofgeneral.inf.ed.ac.uk/trac/

At the moment there is #298, #300 affecting Isabelle, and perhaps #299 
if someone can give a test case.  Please add more if there are others.

> 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.)

Yes, this buggy operating system release was annoying.  It has been 
fixed now, I have working Emacs versions on my Ubuntu 9.10 laptop after 
the latest updates.

https://bugs.launchpad.net/ubuntu/+source/emacs-snapshot/+bug/415101

  - David

-- 
The University of Edinburgh is a charitable body, registered in
Scotland, with registration number SC005336.