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
_______________________________________________
isabelle-dev mailing list
[email protected]
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
