ProofGeneral Coq-mode

Emacs

ProofGeneral で Coq を使う．

Coq のインストール方法はハイテンションなインストール記事にまかせるとします．
この記事みたいにハイテンションにインストール記事を書こうかとも思ったけどレベルが高すぎます．
Mac にウインドウズ・ベロは無いしw
Mac 版はパッケージから入ります．

困ったのは ProofGeneral 3.5 は Mac 上の Coq と通信すると，なぜかフリーズします．
ためしに Development Ver. を使ってみるとうまく動きました．
なんで?

インストール

上記サイト(Development)から開発版の最新をダウンロードします．
解凍すると，本体ディレクトリと本体ディレクトリへのProofGeneralというシンボリックリンクが現れます．

設定

;; ProofGeneral

(load-file "{展開して現れたProofGeneralディレクトリ}/generic/proof-site.el")
これだけ．

起動

.v の拡張子が付いたファイルを読み込むと自動で coq-mode になります．
ならなければ M-x coq-mode で．
20070806-proofgeneral2.png
↑ みたいに将軍のオッサンが表れます．

主要なコマンド

C-c C-n 1ステップ評価
C-c C-Enter カーソル位置まで評価
C-c C-a C-o SearchPattern
C-c C-a C-p Print
C-c C-a C-c Check

あと，ウインドウの上部にアイコンメニューが表示されたりもしてます．
Emacs 使いにとっては CoqIDE より便利なことは間違いないです．

これでモリモリ証明できるね!

20070806-proofgeneral.png