Coq のバージョンアップに対応する
Coq のバージョンが上がってしまい (Homebrew で 何も考えずに upgrade をかけてしまった) 、いざ Coq を書こうとしてRequire Import [ライブラリの名前]
という行を読み込もうとしたら、
Error: File /Users/(略).vo has bad magic number 8700 (expected 8800). It is corrupted or was compiled with another version of Coq.
というエラーが出てしまったのでどうにかしましょうね、という話です。
環境
解決策① Coq を旧バージョンに戻す
Homebrew で Coq を入れているので、バージョンを戻せばなんとかなります。新しいバージョンを入れたばかりなら旧バージョンもローカルに残っていると思うので、とりあえず確認してみます。
$ brew info coq coq: stable 8.8.0 (bottled), HEAD Proof assistant for higher-order logic https://coq.inria.fr/ /usr/local/Cellar/coq/8.7.2 (4,312 files, 217.9MB) Poured from bottle on 2018-02-19 at 13:33:15 /usr/local/Cellar/coq/8.8.0 (4,398 files, 220.6MB) * Poured from bottle on 2018-05-03 at 10:34:53 From: https://github.com/Homebrew/homebrew-core/blob/master/Formula/coq.rb (…以下略)
8.7.2 と 8.8.0 の2バージョンあるのがわかります。また、現在使われているバージョンである 8.8.0 の方に*
印が付いています。
すでに 8.8.0 にしてしまったものを 8.7.2 に戻すには、次のようにします。
$ brew switch coq 8.7.2 Cleaning /usr/local/Cellar/coq/8.8.0 Cleaning /usr/local/Cellar/coq/8.7.2 27 links created for /usr/local/Cellar/coq/8.7.2
下のサイトを参考にさせていただきました: qiita.com
解決策② 新バージョンでライブラリを make し直す
新バージョンで使っていくためには、(ライブラリがうまく対応していればという条件付きですが) 再度コンパイルし直せば大丈夫のようです。
ライブラリのあるディレクトリ(= Makefile が置いてあるディレクトリ) に移動して、
$ make clean
とすれば今までコンパイルされていたもの (主に拡張子が .vo
のファイル) が削除されます。そして、新しいバージョンの Coq (今回なら 8.8.0) で
$ make
とします。これで新しいバージョンでのコンパイルがうまくいくはずです。
参考にさせていただきました: http://coq-club.inria.narkive.com/aFqstVbp/ynot