Running Proof General 4.0 on Mac OS X
As of Mac OS 10.4, the Apple-supplied version of Emacs only runs in a terminal window. This will provide only a primitive environment for Proof General. To do better you need to run Proof General from within a version of Emacs ported as a native Mac OS X application or as version of Emacs running under X11.
Please extend this page if you have further hints or tips, or try new Emacs ports/versions.
Native Mac OS X Emacs ports
There are several native Emacs port attempts for the Mac.
- Emacs.app, the official port but without added (Mac) nonsense
- Carbon Emacs, a build from the GNU Emacs CVS with additional packages and Mac tweaks
- latest versions untested, please try and report
- Aquamacs, an even more Mac-like version of GNU Emacs
- tested but not recommended
X11 Emacs
- No longer recommended, native ports are probably more robust and beautiful
- latest versions untested
- however: for heavy symbols users, it may be the only current way to get subscripts or superscripts
Main.PGEmacsOnMacOSX moved from Main.ProofGeneralOnMacOSX on 23 Aug 2006 - 19:06 by DavidAspinall