みずぴー日記

陽気なプログラマが世界を廻す

ssreflectインストール方法まとめ(Windowsもあるよ!)

f:id:mzp:20140426135019j:plain

「春は証明をはじめる季節」と某氏*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。

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:@さんです

*2:なぜか参加登録したよりも多くの人が来ました