Which of these code samples looks better? This one:

Theorem a : False -> forall n, exists m, n + m = 0.
  intros.
  inversion H.
Qed.

Or this one?

Theorem a : False -> forall n, exists m, n + m = 0.
  intros.
  inversion H.
Qed.

See, I’ve been doing a lot of work in Coq lately, and that second sample is way more appealing to me. So naturally, I want Emacs to display my Coq source like that! Can’t be that hard, right?

Thunder cracks; a wolf howls in the distance; an organist plays several ominous chords.

Turns out Emacs 24.4 has built-in support for exactly this kind of thing! Let’s add a few lines to our .emacs (or a file it loads, or whatever):

(global-prettify-symbols-mode 1)
(setq coq-symbols
  '(("forall" ?∀)
    ("->" ?→)
    ("exists" ?∃)
    ("=>" ?⇒)
    ("False" ?⊥)
    ("True" ?⊤)))

(add-hook 'coq-mode-hook
          (lambda ()
            (setq prettify-symbols-alist coq-symbols)))

This works great–Emacs is happy, Coq is happy, and my buffers have beautiful unicode symbols in them. Except I start to notice something weird…

See how the cursor is just a little taller when it’s hovering over the ∀ symbol? That means that the height of the symbol is different from the height of the rest of the glyphs in the font, meaning that there ends up being more space between lines when one of them has a ∀. Worse, some of the glyphs are a different width!

This happens because the font I use (Inconsolata) doesn’t include glyphs for those symbols, so Emacs finds them in some other font. Try as I might, I could not find a good programming font with good support for math symbols.

So I made my own…kind of. Inconsolata is open-source, so I downloaded this crazy application called FontForge and went to work. Despite my total lack of graphics chops, I was able to add the glyphs shown above (∀, →, ∃, ⇒, ⊥, and ⊤). I designed the arrows myself (with a lot of help from my friend Pavel), copied the uptack and downtack from Courier, and rotated the A and E glyphs to make ∀ and ∃. The results:

See? That wasn’t so hard.

I threw the font and the source up on GitHub. Please add some glyphs, improve the ones already there, and submit a pull request!