[isabelle-dev] Proof General 4.1 on Mac OS X

[Makarius]

On Fri, 21 Jan 2011, Mamoun FILALI-AMINE wrote:

> a remark: previously, there was aquamacs instead of emacs? I find 
> auqamacs more convenient than emacs.

In recent Isabelle releases the default combination was Proof General 
3.7.1.1 with Aquamacs based on Emacs 22.  That turned out as half-decent, 
half-working -- after many weeks of desparate search in the Mac OS X 
ecosphere.

In Isabelle2011 the default Proof General is going to be 4.1, which has 
quite different Emacs requirements, and generally quite different 
behaviour concerning special symbols etc.


So far, I did not spend much time to try all possible combinations of 
Emacsen with PG 4.1.  According to ProofGeneral/COMPATIBILITY, plain GNU 
Emacs 23.2 is recommended (aka the "no nonsense version").  Aquamacs 2.1 
is also based on that code base, so it could in principle work as well, 
despite fancy additions.

When I've tried the slightly older Aquamacs 2.0 some months ago, it turned 
out much slower than plain GNU Emacs 23 -- see also 
http://proofgeneral.inf.ed.ac.uk/trac/ticket/324 -- but that might be 
obsolete in several respects.


I hope to get more concrete feedback from Mac users.  So far I've mainly 
found out that most people are stuck with very old versions of Proof 
General, sometimes even in combination with ancient XEmacs.


 	Makarius