Arantium Maestum

プログラミング、囲碁、読書の話題

spacemacsにcoq layerを入れた

Coq Spacemacs

というわけでemacsでcoq環境を整備したのでメモ。

インストールが必要だったもの：

  • coq
  • proof general
  • spacemacs-coq

前提として

  • spacemacs
  • opam

は入っているものとする（opamはOCamlのパッケージマネジャー）

coq

coq本体は

opam install coq

で入る。

proof general

Proof GeneralはcoqをEmacsからアクセスできるようにするインタフェースを提供する、らしい。（ただしCoqに限らないgeneric interfaceだという説明がある。Isabelleなども使えるようだ）

proofgeneral.github.io

インストールに関しても説明はあるのだが

Skip this step if you already use MELPA. Otherwise, add the following to your .emacs and restart Emacs

と書いてあって、具体的にどの部分が"this step"なのか一見してわかりにくかった・・・　指示を箇条書きにしてくれればわかりやすいかなーと思うのだが・・・

とりあえずMELPAがあるならM-x package-refresh-contents RETとM-x package-install RET proof-general RETしておけば問題なくインストールできるようだ。

spacemacs-coq

Proof Generalとcompany-coqをcoq layerとしてspacemacsで使えるようにする設定集。（company-coqというのはcoq関連の補完や表示の整備、定義へのジャンプなどの機能を追加する拡張）

github.com

~/.emacs.d/privateにgit cloneした・・・　だけではダメで、~/.emacs.d/private/spacemacs-coqというディレクトリ名を~/.emacs.d/private/coqに変えてやる必要がある。

さらにmelpaを使ってProof Generalをインストールした場合、このレポジトリのデフォルトのままではうまくいかない。

このPRにある通り、proof generalのパスを指定している箇所を削除する必要がある：

github.com

その後~/.spacemacsのdotspacemacs-configuration-layersにcoqと追加してやればいい。

これで再起動してcoqがSpacemacs上で使えるようになった。

ただし何故か.v拡張子のファイルを開いてもcoq-modeに自動的にならない。今のところは手動でcoq-modeに移行させていて問題なく使えているが、今後の要調査事項である。

これで四月はSoftware Foundationsの第1巻を進めていきたい。

追記：

@fetburner さんの設定も非常に参考になる（ありがとうございます！）：