martinescardo / HoTT-UF-Agda-Lecture-Notes

Lecture notes on univalent foundations of mathematics with Agda
GNU General Public License v3.0
218 stars 18 forks source link

What font to use in Emacs? #30

Open banbh opened 9 months ago

banbh commented 9 months ago

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: image

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: image

DejaVu Sans Mono

Better looking blackboard bold "N" but lots of missing characters. image

DejaVu Math TeX Gyre

Has all characters but does not seem to be a monospace font: image

Lucida Bright

Has all characters but does not seem monospaced: image

I also tried Lucida Console but many characters were missing.

Monokai

Missing lots of characters: image

JuliaMono

Has all characters and is monospaced: image

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

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:

  1. Does DejuVu Sans Mono work better for other people?
  2. The Agda code block I included at the start of this renders perfectly in my browser. What font is Chrome actually using?
martinescardo commented 9 months ago

Thanks! I have this in my .emacs on a mac:

(set-fontset-font "fontset-default" nil
                  (font-spec :name "DejaVu Sans Mono"))
(set-fontset-font t nil (font-spec :size 20 :name "Symbola"))
banbh commented 9 months ago

Mirroring the config of @martinescardo, I downloaded Symbola, installed Symbola_hint.ttf and added the following to my .emacs (on my Windows machine the sizes matched better if I omitted any :size).

(set-fontset-font "fontset-default" nil (font-spec :name "DejaVu Sans Mono"))
(set-fontset-font t                 nil (font-spec :name "Symbola"))

It looks like image which I think is nicer looking than JuliaMono. I think I would recommend this config over my original one.

My current config is:

;; See https://agda.readthedocs.io/en/latest/getting-started/installation.html#step-3-running-the-agda-mode-program
(load-file (let ((coding-system-for-read 'utf-8))
                (shell-command-to-string "agda-mode locate")))

;; based on https://idiocy.org/emacs-fonts-and-fontsets.html
(set-face-attribute 'default nil :font "DejaVu Sans Mono")
(set-fontset-font t nil "Symbola" nil 'append)

(set-face-attribute 'default nil :height 120)

followed by some custom-set-variables.