Proof GeneralでCoq
プログラミング Coqを参考に、CoqとCoqIDEを入れて試してみたが、
どうもCoqIDEの動きがおかしい。時々固まったり変な動作をする。
周りの人に相談したところ
「CoqIDEは使いものにならないからProof Generalを使え」
と言われたのでProof Generalとやらを入れてみた。
Emacs上で動く便利なものらしい。
以下はただのメモ書き。
* ダウンロード *
公式サイトからダウンロードする。
現時点のバージョンは4.0のようだ。
* インストール *
公式サイトの説明に従い、ファイルを展開して、
.emacsにload-fileを追加。
試しにEmacsで拡張子がvのファイルをひらいてみるが、
「Emacsのバージョンが23.1じゃないからダメ」
と怒られる。これまた公式サイトの説明に従いmake。
make clean make compile EMACS=`which emacs`
しかし、make時にエラーが起こる。
「`font-lock-beginning-of-syntax-function’はobsoleteだから’syntax-begin-function’を使え」
と言ってるようなので、何も考えずにソースコード中の
font-lock-beginning-of-syntax-functionをsyntax-begin-functionに置換。
makeはこれで通った。
* 起動 *
Emacsで拡張子がvのファイルを開くと自動的にProof Generalが立ち上がる。
公式サイトのマニュアルを適当に眺めたところ、
- C-c C-nで証明をひとつ進める
- C-c C-uで証明をひとつ戻す
らしい。今の私の知識ではどうせこれしか使わない。後のものは後で覚えよう。
C-c C-RETでカーソルの位置まで証明を進めるみたいだが、
これをやろうとすると「C-c RET is undefined」と言われてしまう。
controlを押しながらreturnを押してるはずなんだけど、なんでだろう。
まあ、誰か詳しい人が解決法を教えてくれるだろう。
* 疑問点 *
CoqIDEでは「Eval simpl in xxx」みたいなものを、
専用の場所に書いていたけど、Proof Generalではどこに書けばいいんだろう。
ソース中に書いたら動いたけど、ソースとは分離したい。