Macでssreflect
以下はssreflectをMacで動かそうとした悪戦苦闘の記録です。
最終的には、以下のような構成になりました。
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を使ってる関係上、微妙に異なります。
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)))))
