ssreflectインストール方法まとめ(Windowsもあるよ!)
「春は証明をはじめる季節」と某氏*1がよくわからないことを言いだしたので、Modern Coqことssreflectの勉強会を開催しました。(スタートssreflect #1)
勉強会にはだいたい30人くらいの方が参加し*2、全員がssreflectを使った証明を実際に行いました。そのため、30個の様々な環境にssreflectがインストールされたわけなので、その結果をまとめておきます。
元データ
https://docs.google.com/spreadsheets/d/1X_vRVO3eizebOyG4tjcChzUZofrE9AGWwMEqUCyKKHs/edit?pli=1#gid=0
Windowsの場合
自分でビルドするのは地獄の道らしいので、コンパイル済みのバイナリを使います。ssreflectはMicrosoft製なだけあって、Windowsが一番インストールが楽ですね:D。
- Coq http://coq.inria.fr/download
- ssreflect for Windows https://twitter.com/qnighy/status/454981287145512960
非Windowsの場合
ディストリビューション標準のパッケージマネージャの利用
一部のパッケージマネージャでは、ssreflectのパッケージが用意されています。 特に理由がなければそれを使いましょう。
Debian Jessie/ Ubuntu 14.04の場合:
$ apt-get install ssreflect
Mac OS X(Homebrew)の場合:
$ brew install ssreflect
Gentooの場合は、proof overlayを追加した上で:
$ emerge ssreflect
OPAMの利用
ssreflectのパッケージがない(or バージョンが古い)場合は、自分でssreflectをビルドする必要があります。 ただ、その場合でもOCamlのパッケージマネージャであるopamを利用すれば、Coqのビルドまでは自動化できます。
OPAM - Quick Installを参考にOpamをインストールした後、Coqをインストールします。
$ opam install coq
その後、https://gforge.inria.fr/frs/?group_id=401 からssreflect-1.4-coq8.4.tar.gzをダウンロードし、適当なディレクトリに展開しビルドします。
$ cd ssreflect-1.4 $ make $ make install
全部自分でビルド
https://github.com/suharahiromichi/doc/blob/master/cs_ssr_install.md あたりが参考になります。 面倒なのであんまりお勧めしません。
*1:@yoshihiro503さんです
*2:なぜか参加登録したよりも多くの人が来ました