きくらげ観察日記

好きなことを、適当に。

coq-modeとproofgeneralでcoq環境を作る

EmacsでCoqを扱う場合、proofgeneralというものを使うのが一般的らしいです。

$ sudo apt-get install coq proofgeneral

Ubuntuの場合はどちらもaptのリポジトリに入っているので、上のコマンドを打つだけでインストールは完了です。

(load-file "/usr/share/emacs/site-lisp/proofgeneral/generic/proof-site.el")

上のコードを.emacs.elに追加することによってproofgeneralを読み込むことができます(Ubuntuの場合。パスは適宜読み替えてください。)

f:id:cloudear8:20161005151320p:plain