coq環境作って使う emacs + ProofGeneral

そもそもはProofGeneralが使いたいがためにEmacsを使い始めたが、とりあえずAgdaをやめてCoqをいじるようになった今、vimscripts/coq_IDEというやつでもいいかもしれないと思い始めているが・・・

Macでの導入は簡単。

homebrewを使う.もう何でもこれに頼ってしまう。

まずはcoqを入れよう

brew install coq

恐らくインストールすると、こんな感じ（↓）でemacsでのcoq modeについての説明が出るはず。

Coq's Emacs mode is installed into
  /usr/local/opt/coq/lib/emacs/site-lisp

To use the Coq Emacs mode, you need to put the following lines in
your .emacs file:
  (setq auto-mode-alist (cons '("\\.v$" . coq-mode) auto-mode-alist))
  (autoload 'coq-mode "coq" "Major mode for editing Coq vernacular." t)

これに従って設定ファイルに設定を追記する。

これで.vという拡張子のファイルをcoqとして認識して、coq modeに入ってくれるようになる。

続いてProofGeneral.

brew info proof-general
proof-general: stable 4.2
http://proofgeneral.inf.ed.ac.uk
/usr/local/Cellar/proof-general/4.2 (257 files, 4.2M) *
  Built from source
From: https://github.com/Homebrew/homebrew/blob/master/Library/Formula/proof-general.rb
==> Options
--with-doc
        Install HTML documentation
--with-emacs=
        Re-compile lisp files with specified emacs
==> Caveats
To use ProofGeneral with Emacs, add the following line to your ~/.emacs file:
  (load-file "/usr/local/share/emacs/site-lisp/ProofGeneral/generic/proof-site.el")

--widh-emacs=のオプションが気になりつつ一旦無視して入れてみると、後でNotice見たいのがでた。

なのでちゃんと指定して入れる方法を書いておく

brew install --with-emacs=`which emacs` proof-general

これでよい。

で、入れたらbrew infoした時に出ているようにemacsの設定ファイルにProofGeneralを読み込む設定を書く

To use ProofGeneral with Emacs, add the following line to your ~/.emacs file:
  (load-file "/usr/local/share/emacs/site-lisp/ProofGeneral/generic/proof-site.el")

.emacsなりinit.elなりに、以下を追加する。環境や設定によってはインストールされる場所が変わったりするのかな？その場合は多分brew installした後に出る気がする

で、proof-generalはこれでよし。

これでcoqファイルを開いた時に、将軍のsplashが表示されるようになって、証明する時に使えるようになる！

f:id:totem_3:20141115094738p:plain