homebrew で MathComp を入れる
追記 2015/11/11
今だったら公式の opam リポジトリから入れたほうが簡単にマルチコアを使えて速いし安心だと思います。
opam repo add coq-released https://coq.inria.fr/opam/released # opam に Coq 関連のライブラリを追加 opam install -j4 coq.8.4.6 coq:ssreflect.1.5.0 coq:math-comp.1.5.0 # 安定版を指定してのインストール
MathComp (mathematical components) は Coq の拡張である SSReflect を使った、数学系の問題に特化したライブラリです。
で、Mac でよく使われているパッケージマネージャである homebrew には coq も ssreflect も標準であるのに、なぜか mathcomp はありません。homebrew の ssreflect formula は ssreflect-1.4 以前からあり、ssreflect は 1.5 から ssreflect と mathcomp の2つに分かれたのであってもいいはずなのですが、なぜかありません。
なので formula を作りました。
amutake/homebrew-mathcomp · GitHub
% brew tap amutake/mathcomp % brew update # 最新の ssreflect が必要なので % brew install mathcomp
これで mathcomp が入ります。mathcomp は ssreflect に依存しているので、ssreflect も入るようになっています。mathcomp のインストールは1時間くらいは普通にかかるので、気長に待ちましょう。
ところで homebrew の formula って依存パッケージのバージョンは指定できないんでしょうか…この場合だと ssreflect-1.5 が必要なので…
