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.

  •, the official port but without added (Mac) nonsense
    • tested and recommended
  • 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
Topic revision: r8 - 10 Oct 2010 - 13:20:35 - DavidAspinall
Main.PGEmacsOnMacOSX moved from Main.ProofGeneralOnMacOSX on 23 Aug 2006 - 19:06 by DavidAspinall
This site is powered by the TWiki collaboration platformCopyright © by the contributing authors. All material on this collaboration platform is the property of the contributing authors.
Ideas, requests, problems regarding TWiki? Send feedback
This Wiki uses Cookies