事情があって、AgdaかCoqを触ってみようか、と。
WindowsマシンへのAgdaのインストールはうまくいきませんでした。次の記事にあるような状況らしいですが、かなり萎えます。
- http://d.hatena.ne.jp/kiiiino3+lab/20141114/1415947022
- http://d.hatena.ne.jp/kiiiino3+lab/20141128/1417152643
- http://d.hatena.ne.jp/kiiiino3+lab/20141205/1417740917
上記木下さんの最後の記事（昨日書かれたもの）にあった http://wiki.portal.chalmers.se/agda/pmwiki.php?n=Main.Windows から Agda-2.3.0.1-20121108-setup.exe をダウンロードすると、Nortonが速攻で削除してくれます。面倒になってCoqに。
Coq
今日の時点で、
- The current version: Coq 8.4pl5
https://coq.inria.fr/download から、coq-installer-8.4pl5.exe をダウンロードできます。
-a--- 2014/12/05 0:48 54961995 coq-installer-8.4pl5.exe
このインストーラーを実行するだけでインストールは終わりです。パスの設定はしてくれないので、手動でパスを設定。
$ coqtop --version
The Coq Proof Assistant, version 8.4pl5 (November 2014)
compiled on Nov 07 2014 18:14:16 with OCaml 3.11.2$ coqtop
Welcome to Coq 8.4pl5 (November 2014)Coq < Quit.
$
これでOK。簡単でした。
Proof General
Emacsで使いたいのでProof Generalをインストール。http://proofgeneral.inf.ed.ac.uk/download からダウンロードできます。http://proofgeneral.inf.ed.ac.uk/releases/ProofGeneral-4.2.tgz を直接HTTP GETしてもいいでしょう。
-a--- 2014/12/05 23:53 1613190 ProofGeneral-4.2.tgz
tarコマンドでファイルを展開しようとすると、シンボリックリンクがあるのでうまくいかない。
[追記]シンボリックリンクのせいというよりは、下に書いているように、元ファイルがないのがエラーの原因のようです。シンボリックリンクだけなら、（tarコマンドの仕様にもよりますが）Windows上でも頑張ってリンクを作るとか、コピーしてしまうとかはできますからね。[/追記]
Emacsはtarファイル（tgzでも）を閲覧できるので、眺めてみると：
lrwxrwxrwx da/da 0 ProofGeneral-4.2/doc/ProofGeneralPortrait.eps.gz --> ../web/ProofGeneralPortrait.eps.gz lrwxrwxrwx da/da 0 ProofGeneral --> ProofGeneral-4.2
シンボリックリンクが2つあるようです。ProofGeneral-4.2/doc/ProofGeneralPortrait.eps.gz と ProofGeneral は無視しよう。
$ tar xvf /c/Installed/ProofGeneral-4.2.tgz --exclude=ProofGeneral-4.2/doc/ProofGeneralPortrait.eps.gz --exclude=ProofGeneral
リンク先であるProofGeneral-4.2/web/ProofGeneralPortrait.eps.gz というファイルがそもそも存在しません。なくても実害はないだろうと放置。
僕は、~/.emacs.d/modules/ProofGeneral-4.2/ というディレクトリにファイル群を展開しました。INSTALL文書に従って、.emacs（いまどきはinit.elでしょうが）に次の１行を追加します。
(load-file "~/.emacs.d/modules/ProofGeneral-4.2/generic/proof-site.el")
http://logic.cs.tsukuba.ac.jp/~kam/lecture/complogic2014/coq-howto.html には次の設定も書いてありました。追加したほうがいいのかも知れません（まだ意味が分からない）。
(defadvice coq-mode-config (after deactivate-holes-mode () activate) "Deactivate holes-mode when coq-mode is activated." (progn (holes-mode 0)) ) (add-hook 'proof-mode-hook '(lambda () (define-key proof-mode-map (kbd "C-c C-j") 'proof-goto-point)))
サンプルの ~/.emacs.d/modules/ProofGeneral-4.2/coq/example.v ファイルを読むと、Coqモードにはなってくれたのですが、
Warning (emacs): Proof General compiled for GNU Emacs 24.2 but running on GNU Emacs 23.4: "make clean; make" is recommended.
あ、そうか、今使っているのはGNUPACKのEmacs 23か。
(emacs-version) "GNU Emacs 23.4.1 (i386-mingw-nt6.1.7601) of 2012-02-05 on GNUPACK"
Emacs 24をインストールしたことはあるのだけど、日本語入力で問題があるようでしたので変える気がしない。ともかく指示に従って make clean; make しましょう。
****************************************************************
Byte compiling...
****************************************************************
make elc
make[1]: Entering directory `/cygdrive/c/Users/hiyama/Work/.emacs.d/modules/Proo
fGeneral-4.2'
emacs --batch --no-site-file -q -eval '(setq load-path (append (mapcar (lambda
(d) (concat "/cygdrive/c/Users/hiyama/Work/.emacs.d/modules/ProofGeneral-4.2/" (
symbol-name d))) (quote (acl2 ccc coq hol98 isar lego hol-light phox pgshell pgo
caml pghaskell generic lib contrib/mmm))) load-path))' -eval '(progn (require (q
uote bytecomp)) (require (quote mouse)) (require (quote tool-bar)) (require (quo
te fontset)) (setq byte-compile-warnings (remove (quote cl-functions) (remove (q
uote noruntime) byte-compile-warning-types))) (setq byte-compile-error-on-warn t
))' -f batch-byte-compile acl2/acl2.elIn toplevel form:
acl2/acl2.el:14:1:Error: Cannot open load file: proof-easy-config
make[1]: *** [acl2/acl2.elc] Error 1
make[1]: Leaving directory `/cygdrive/c/Users/hiyama/Work/.emacs.d/modules/Proof
General-4.2'
make: *** [compile] Error 2$
バイトコンパイルがうまくいかない。たぶんファイルパス名の問題だと思いますが、もういいや、手動でバイトコンパイルしよう。
なぜかEmacsには、byte-compile-directoryというコマンドはなくて、byte-recompile-directory に数値引数を渡すという分かりにくい仕様： Emacsで.elファイルがあるディレクトリを探して、そこで C-u 0 M-x byte-recompile-directory していきます。そしたら、
Compiling file c:/Users/hiyama/Work/.emacs.d/modules/ProofGeneral-4.2/coq/coq-mmm.el at Sat Dec 06 16:25:03 2014
coq-mmm.el:15:1:Error: Cannot open load file: mmm-auto
ロードバスが足りてないみたい。mmm-auto.elは ~/.emacs.d/modules/ProofGeneral-4.2/contrib/mmm/ にあったので、(add-to-list 'load-path (expand-file-name "~/.emacs.d/modules/ProofGeneral-4.2/contrib/mmm/")) しておきます（最近は expand-file-nameは不要かも）。
僕は通常、Emacsツールバーを使わないのですが、Coqモードではツールバーがあったほうが便利かも知れません。
(tool-bar-mode 1)
あー疲れた。
