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.

というエラーが出てしまったのでどうにかしましょうね、という話です。

環境

  • macOS HighSierra 10.13.4
  • Emacs + Proof General
  • Coq version 8.7.2 → 8.8.0 (Homebrew)

proofgeneral.github.io

解決策① 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