はじめに
定理証明支援系Rocq(旧Coq)とそのライブラリであるmathcompをMacのパッケージマネージャーの1つであるHomebrewのみを用いてインストールする方法を解説します。
本記事作成時の状況
Homebrew 5.0.8
Rocq 9.1.0
mathcomp 2.5.0
(Ocaml 5.3.0)
手順
Homebrewがインストールされている状態を仮定します。
確認方法はターミナルを開き、以下のコマンドを実行します。
brew --version
もしエラーが出る場合は上のリンクからHomebrew本体を入手し、ターミナルを再起動してください。
Rocq本体のインストール
まず、ターミナルで次のコマンドを実行します。
brew install math-comp
これでRocq本体とそのライブラリであるmathcompがインストールできます。
環境変数の設定
今、Homebrewで入れたrocqコマンドのパスを確認するために、次のコマンドを実行します。
which rocq
すると次のようなパスが出てきます。(パスは環境によって変わる可能性があります)
/usr/local/bin/rocq
このbin以前のパスを{*path*}(上の例では/usr/local)とします。
そのとき、次の文をシェルの環境設定ファイル(例えば~/.zshrcなど)に追記します。(無い場合は作成する)
export OCAMLPATH="{*path*}/opt/rocq-elpi/libexec/lib:$OCAMLPATH"
これを追記する理由はppx_deriving.runtimeのパスが通っていないからです。
このパスは本当はテスト環境{*path*}/optのものなのですが、本番環境{*path*}/libの方にはなぜかインストールされていないので上記のように書くことでテスト環境のパスを通します。
（なので実はbrew test math-comp自体はこれを書かなくても通ります)
その後、ターミナルを再起動することでrocqコマンドがうまく使えるようになりました。
動作確認方法
次のRocqプログラムをコンパイルしてみます。
From mathcomp Require Import all_boot.
(* 上記のppx_deriving.runtimeがないと通らない *)
このプログラムを以下のコマンドでコンパイルできたら成功です。
rocq c example.v
emacsのインストール
エディタであるemacsとProof Generalを入れます。
まずはemacsのインストール方法です。
brew install --cask emacs
環境変数の設定
次に、~/.emacsファイルに次の文を追加します。(無い場合は作成する)
(exec-path-from-shell-initialize)
(exec-path-from-shell-copy-envs '("PATH" "OCAMLPATH"))
その後、emacsを立ち上げて次のコマンドを実行します。
M-xを押し、package-installと入力しenter、その後exec-path-from-shellと入力します。
(M-xはOption + x)
これによって.zshrcの環境変数をemacsに引き継ぎます。
今、OCAMLPATHの設定を追加したので、これをemacsにも引き継ぐようにしています。
Proof Generalのインストール
Proof Generalを公式の手順の通りに入れます。1
~/.emacsファイルに次の文を追加します。
(require 'package)
(add-to-list 'package-archives '("melpa" . "https://melpa.org/packages/") t)
(package-initialize)
次にemacsを立ち上げます。
M-xを押してpackage-refresh-contentsと入力してenter
M-xを押してpackage-installと入力してenter、proof-generalと入力します。
(M-xはOption + x)
emacsを再起動することで、Proof Generalが使えるようになります。
まとめ
証明支援系RocqとそのライブラリmathcompをHomebrewから直接インストールする方法について解説しました。
これ以降は試行錯誤の記録となります。
試行錯誤の記録
本記事作成の背景
Rocqをインストールするのに今使っているopamのバージョンが古くて非対応であり、その差分の更新に色々と手こずったのが背景としてあります。
- homebrewでopamをver2.0.7からver2.5.0にupgredeしたはずなのですが、
opam --versionを実行すると相変わらずver2.0.7と表示されたりします。 - そこで
brew uninstall opamでopamをアンインストールしてもなぜかまだopamコマンドが使えたりします。(もちろんどちらもターミナルを再起動してみました) - アンインストール後もopamコマンドが使える現象は他にも報告があるみたいです。
- opamを直接入れたのかもと思い、実行ファイルを削除して無理やり消去、Homebrewから再インストールでver2.5.0にアップデートしてみたら、今入れているライブラリがver2.0以下でないといけない縛りがあるらしく、ver2.5.0にアップデートすると新たにライブラリをインストールできなくなりました。
ずっと古いCoqを使い続けていた大きな理由がこれです。
opamでの管理が面倒に感じてしまったため、バージョン管理は全てHomebrewで統一してしまうのが楽だろうというのが本記事作成の動機でした。
そのままインストールしてみると
公式にもある通り
brew install rocq
これでRocq本体がインストールでき、mathcompライブラリも同様に
brew install math-comp
でインストールできるはずです。
しかしながら適当なファイルをコンパイルしようとすると
From mathcomp Require Import all_ssreflect.
(* Coqファイルを流用しているのでall_ssreflectにしていますが、Rocqだと本当はall_bootの方がいいです。all_bootに変えてもエラーが出るのは同じです。 *)
の部分を実行しようとすると次のエラーが出ます。
Error:
Findlib error: ppx_deriving.runtime not found in:
/usr/local/lib/ocaml/coq/../rocq-runtime/..
/usr/local/lib/ocaml
ppx_derivingはOcamlのライブラリでopamからはインストールできますが、残念ながらHomebrewからは不可能なようでした。
テスト環境だとうまくいく
しかしながら
brew test math-comp
を実行すると
From mathcomp Require Import ssreflect seq.
という一文があるにも関わらず成功します。
testing.vを含むコンパイルプログラムのソース
そこで、通常の環境とテストの実行環境を比較してみると
通常のrocqコマンドは/usr/local/bin/rocqが実行されますが、
テスト環境のrocqコマンドは/usr/local/opt/rocq/bin/rocqが実行されることが分かりました。
また、問題になっているppx_derivingですが、
通常参照する/urs/local/lib/ocaml/rocq-elpi内には存在しませんが、
テスト環境の/usr/local/opt/rocq-elpi/libexec/lib内にありました。
なので、このパスを通せば上手くいくハズです。
他サイトを参考にしてみる
同じ状況の似たような事例もあり、Coq8.8.2までは大丈夫でCoq8.9.0以降がこの状態になっているっぽいです。
特にRequire ImportやRequire Export部分でエラーが起きるみたいです。
ちなみに以下のプログラムだけならエラーが出ずに通りました。
Definition double_add1 (n:nat) := n * 2 + 1.
別のサイトでは
brew install coq
の代わりに
brew install coq --build-from-source
だと上手くいくという話ですが、こちらの方法も現バージョンだと状況は変わらず。
時系列でみると
20xx年x月 Coq 8.8.2では正常に動く？
2019年2月 Coq 8.9.0以降でエラーが発生する
2022年10月 --build-from-sourceオプションを入れることで回避できた
2026年1月 それも不可能になった
といった感じみたいです。
質問サイトに投げてみる
Rocq公式コミュニティでこの件に関する質問を投げてみたら、どうやらrocq-elpiの環境変数に問題がありそうだということが分かりました。
しかしながら通すパスが*{opt_libexec}/libと書いてあり、変数opt_libexecの値が具体的にどのパスなのかが分からなかったです。
以上、試行錯誤の様子でした。
-
Homebrewから
brew install proof-generalで導入する方法もありますが、このコマンドだけではすぐ使えるようにはならず、依存パッケージも多いのであまりオススメしないです。 ↩