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 分ちょっとでコンパイルが終わった。