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
  • 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
  • latest versions untested
  • however: for heavy symbols users, it may be the only current way to get subscripts or superscripts
    • See http://proofgeneral.inf.ed.ac.uk/trac/ticket/338