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

f:id:mzp:20140426135019j:plain

「春は証明をはじめる季節」と某氏*1がよくわからないことを言いだしたので、Modern Coqことssreflectの勉強会を開催しました。(スタートssreflect #1)

勉強会にはだいたい30人くらいの方が参加し*2、全員がssreflectを使った証明を実際に行いました。そのため、30個の様々な環境にssreflectがインストールされたわけなので、その結果をまとめておきます。

自分でビルドするのは地獄の道らしいので、コンパイル済みのバイナリを使います。ssreflectはMicrosoft製なだけあって、Windowsが一番インストールが楽ですね:D。

一部のパッケージマネージャでは、ssreflectのパッケージが用意されています。特に理由がなければそれを使いましょう。

Debian Jessie/ Ubuntu 14.04の場合:

$ apt-get install ssreflect

Mac OS X(Homebrew)の場合:

$ brew install ssreflect

Gentooの場合は、proof overlayを追加した上で:

$ emerge ssreflect

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 あたりが参考になります。面倒なのであんまりお勧めしません。

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

みずぴー日記