このブログの更新は Twitterアカウント @m_hiyama で通知されます。
Follow @m_hiyama

メールでのご連絡は hiyama{at}chimaira{dot}org まで。

はじめてのメールはスパムと判定されることがあります。最初は、信頼されているドメインから差し障りのない文面を送っていただけると、スパムと判定されにくいと思います。

参照用 記事

WindowsへのCoqのインストール

事情があって、AgdaかCoqを触ってみようか、と。

WindowsマシンへのAgdaのインストールはうまくいきませんでした。次の記事にあるような状況らしいですが、かなり萎えます。

上記木下さんの最後の記事(昨日書かれたもの)にあった 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でしょうが)に次の1行を追加します。

(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.el

In 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)

あー疲れた。