環境
- Mac OSX Yosemte 10.10.5
- Homebrew 1.1.2
- Homebrew/homebrew-core (git revision a06e; last commit 2016-11-29)
- GNU Emacs 25.1.1
- Agda 2.5.1.2
Agda のインストール
Homebrew が直接 formula を提供しているので
- $ brew install agda
だけでOK。便利。
Agda の設定
- $ agda-mode setup
するか、その時に表示される
(load-file (let ((coding-system-for-read 'utf-8))
(shell-command-to-string "agda-mode locate")))
を ~/.emacs や ~/.emacs.d/init.el なりに書いておくとOK。
なんと便利なことに bottle の agda には std-lib が同梱されているので、いきなり open import Relation.Binary.PropositionalEquality とか書いて使うことができます。
特殊文字(Unicode の East Asian Ambiguous) の設定
素の emacs では agda-mode で利用する特殊文字(∏ など)があると表示が乱れます。
これはいくつかの記号の幅が固定されておらず、国によって幅が定義される文字である East Asian Ambigous 文字がソースに含まれる時に発生する問題です。
日本語フォントは基本的に幅2なのですが、英語では幅1らしい。
設定をしないとEmacsが幅を1で処理するため、表示される日本語フォントの幅と合わずに表示が乱れてしまいます。
これを解決する elisp が hamano/locale-eaw に公開されているようなので使ってみます。
README にあるように eaw.el を ~/.emacs/site-lisp に配置して
(add-to-list 'load-path "~/.emacs.d/site-lisp")
(require 'eaw)
(eaw-fullwidth)
を ~/.emacs なり ~/.emacs.d/init.el に書きます。
そうするとEmacs が特殊文字の幅を2として処理してくれます。
ちなみに Terminal や tmux なども East Asian Ambiguous を幅2に設定するのを忘れないように。
過去に自分で書いた elisp もあるのですが割とその場しのぎで書いていたので、これからは eaw.el を使っていこうかなとか。
