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

Makarius makarius at sketis.net
Wed Nov 11 11:19:55 CET 2009

On Wed, 11 Nov 2009, David Aspinall wrote:

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

There have been other serious problems, but I could not catch up isolating 
them all.  A trac entry like "SMEF on Ubuntu 9.10 x86_64" certainly would 
not help.

I am also struggling again to find a combination of PG + Emacs that works 
on Mac OS.  GNU Emacs 23 somehow fails -- tickets will come when I've 
managed to pin down the problems.


More information about the isabelle-dev mailing list