-
Notifications
You must be signed in to change notification settings - Fork 21
Description
Thank you @martinescardo for creating these notes and making them available. One aspect of these notes that I found attractive was being able to follow along in Agda. This is easier if Emacs is using a font which can render all (or most) of the characters used in the notes. It took me some time to find some candidate fonts and I thought I would document my experience below. The goal of this "issue" is to share what I found as a novice Emacs user on Windows 10.
Summary: JuliaMono seems like a nice choice. There may be other choices (such as DejaVu Mono; however on its own it seems to be missing some characters, so it may require a fallback font.)
I'm using running a stock GNU Emacs 29.1 and my .emacs file consists of code to load agda-mode.
(load-file (let ((coding-system-for-read 'utf-8))
(shell-command-to-string "agda-mode locate")))The example Agda file is
{- Unicode: lambda = Ξ», BB "B" = πΉ -}
{-# OPTIONS --without-K --exact-split --safe --auto-inline #-}
module HoTT-UF-Agda where
variable
π€ π₯ π¦ π£ : Universe
data π : π€β Μ where
β : π
π-induction : (A : π β π€βΜ ) β A β β (x : π) β A x
π-induction A a β = a
data π : π€ββΜ where
data β : π€β Μ where
zero : β
succ : β β βDefault
Before setting a font this is what an example file looks like:

Consolas
I believe the default font used by Chrome for fixed-width text on my machine is Consolas, so I tried it in Emacs by using Options -> Set Default Font. (For all fonts below that's how I will test them.) It looks like:

DejaVu Sans Mono
Better looking blackboard bold "N" but lots of missing characters.

DejaVu Math TeX Gyre
Has all characters but does not seem to be a monospace font:

Lucida Bright
Has all characters but does not seem monospaced:

I also tried Lucida Console but many characters were missing.
Monokai
JuliaMono
Has all characters and is monospaced:

Above was 10pt; perhaps looks better at 12pt:

Conclusion
JuliaMono seemed to work best. I added the following to my .emacs (based on Fonts in Emacs):
(set-face-attribute 'default nil
:family "JuliaMono"
:height 120
:weight 'normal
:width 'normal)Questions
I would be interested in answers to the following questions:
- Does DejuVu Sans Mono work better for other people?
- The Agda code block I included at the start of this renders perfectly in my browser. What font is Chrome actually using?
