Coq 8.5 を入れてみた
先日 Coq 8.5 がリリースされたので入れてみた話。
coq 自体のコンパイルは問題なくできたけど,その後 ssreflect のコンパイルに失敗した。make すると
Error: The files /usr/local/lib/coq/parsing/pcoq.cmi and /usr/local/lib/coq/lib/compat.cmi make inconsistent assumptions over interface Compat
と言われる。問題の compat.cmi はタイムスタンプを見ると Coq の前のバージョンのものらしいことがわかる。どうもソースコードのディレクトリ構成が変わっているようで,新しい compat.cmi は別のディレクトリに存在している。それで Coq を make install したときに上書きされずに古いものが残って,何らかの理由でそれが間違って参照されているようだ。
試しに
sudo rm -fr /usr/local/lib/coq/
してから coq をインストールし直してみると,今度は ssreflect の make に成功した。
mathcomp もコンパイルし直さないといけない。試しに make -j16 とかやってみたら 20 分ちょっとでコンパイルが終わった。