Coq 8.5が公式にリリースされました。
そして、Windows版の SSReflect, MathComp もリリースされました。
早速インストール＆動作確認しました。
基本的にはインストーラをクリックするだけなのですが、
ノウハウとして
入手方法やインストールの方法を
メモしておきます。
気を付けることは、
これまでに Coq と SSReflect, MathComp をインストールしていた場合、
・アンインストールをする
もしくは
・これまでのCoqとは異なるフォルダに
新しい Coq 8.5 をインストールする
ということです。
◆Coq 8.5の入手方法とインストール
Windows版は 32ビット版と64ビット版の二つのインストーラが提供されました。
２０１６年１月２２日現在では、どちらも
https://coq.inria.fr/download
から入手可能です。
ここからインストーラをダウンロードして、起動します。
あとはインストーラの指示に従うだけでOKです。
途中でインストール先を選択する画面が現れます。
上に述べましたが、
もしも他のバージョンの Coq が既にインストールされていたら、
・それらをアンインストールする
もしくは
・Coq 8.5 を他のCoqとは異なるフォルダにインストールする
のどちらかにすると良いでしょう。
◆SSReflect/MathCompの入手方法とインストール
Windows版 Coq 8.5 をインストーラからインストールした場合、
SSReflectやMathCompのバージョンは 1.6 を使うことになります。
こちらにもWindows版インストーラが用意されています。
下のURIからダウンロードできます。
http://ssr.msr-inria.inria.fr/FTP/
インストーラは３２ビット版と６４ビット版の両方が提供されています。
それぞれ
ssreflect-mathcomp-installer-1.6-win32.exe
ssreflect-mathcomp-installer-1.6-win64.exe
という名前がつけられています。
先のURIの先にあるHPの下の方にあります。
インストールはインストーラをクリックするだけでできます。
途中でインストール先を選択する画面が現れます。
その際には、Coq 8.5で指定したディレクトリ名をそのまま指定してください。
以上でインストールは終わりです。
◆動作確認
Coqを起動するには
スタートメニューなどから
CoqIDE
を選んでください。
SSReflect/MathCompを読み込むには
CoqIDEのスクリプトエリアに
From mathcomp
Require Import ssreflect.
と入力し、CoqIDEの一行読み込みボタンをクリックしてください。
上部にあるアイコンのうち、左から３番目の ↓ のことです。
入力した上の２行「From … ssreflect.」が緑色に変われば
正しく動作しています。
