読者です 読者をやめる 読者になる 読者になる

600000007

プログラムと折り紙のブログです。

Macでssreflect

coq ssrefrect

以下はssreflectをMacで動かそうとした悪戦苦闘の記録です。
最終的には、以下のような構成になりました。

  • Mac OS X 10.9.4
  • Emacs 24.3.1
  • ProofGeneral4.2
  • Coq8.4pl4
  • ssreflect1.5

CoqIDE or ProofGeneral

Mac OS X 10.9では、CoqIDE8.4は起動できません。既知の問題みたいです。
操作性も含めてEmacs + ProofGeneralの構成をお勧めします。

Emacs

デフォルトで入っているemacsや、homebrewでインストールしたものをターミナルで使用すると、なぜかgotoによるコンパイル(カーソルがある位置までコンパイルしてくれる)ショートカットが使えませんでした。
Ctrl + C , Enterを実行すると、C-c RET undefinedというエラーになります。
Emacs for Mac OS X なら大丈夫でした。
これはEmacs.appとしてインストールされます。

ssreflectのインストール

homebrewでインストールします。事前にXQuartzのインストールが必要です。
また、ssreflectのダウンロードパスが変わっているので、brew updateを必ずしておいた方が良いです(していなかったせいではまりました・・・)。
# brew update
# sudo brew install ssreflect

clangエラー

初っぱなからclangエラーでつまづきました。
こちら によると、clangのバージョンによる問題だそうです。
xcode5.0.2にダウングレードして回避しました。

ProofGeneralのインストール

ProofGeneralの最新版は4.2ですが、Emacs24系には対応していません。
そのためmakeに失敗すると思いますが、こちらにあった方法で回避できました。Emacs.appの指定方法もこちらにあります。

あとはProofGeneralにssleflectを認識させる必要があります。
Coq/SSReflectの設定にあるようにEmacsの設定変更をするのですが、homebrewとEmacs.appを使ってる関係上、微妙に異なります。

Emacs.appの設定

~/.emacs.d/init.pl を編集します。

ssreflectの場所

パスは/usr/local/Cellar/ssreflect/1.5/lib/coq/user-contrib/Ssreflectになります。

(setq coq-prog-args
(https://staff.aist.go.jp/reynald.affeldt/ssrcoq/install.htmlcons "-R" (cons "/usr/local/Cellar/ssreflect/1.5/lib/coq/user-contrib/Ssreflect" (cons "Ssreflect"
(cons "-emacs" nil)))))

coq topが見つからない

ProofGeneralが正しくインストールされていると、*.vファイルをEmacsで開けば起動されます。
無事起動したので一安心していたら、

Searching for program: No such file or directory, coq top 

というエラーでコンパイルが進みませんでした。
こちら の方法で回避できました。

ここまでくればちゃんと動くはずです!
こちらばっかですね。インターネット万歳。
mathcompはまだコンパイルが終わらないのでまた今度。