Coq/SSReflect/MathCompをインストールしようとした際、やり方が分かりづらくて苦戦したのでメモしておきます。

Windowsでのインストール方法についてまとめました。

はじめに

「Coq/SSReflect/MathCompによる定理証明:フリーソフトではじめる数学の形式化」の勉強を進めるにあたってCoq/SSReflect/MathCompをインストールしようとしたら、インストールが最初にして最大の難所でした(汗)

本にも説明はあり、CoqのインストーラはGitHubで入手できるのですが、Coqとセットで使うSSReflectとMathCompのインストーラが本に載っているサイトにありませんでした（というかサイト自体にアクセスできない）。

いろいろと調べた結果、2つの方法でインストールすることに成功しました。

方法1：旧バージョンのインストーラを利用

一番簡単でおすすめしたいのが、旧バージョンのインストーラを利用する方法です。

なぜ旧バージョンなのかというと、最新版はインストーラ自体がまだできていないからです。なので、最新版を使いたい！という方には方法2のほうをおすすめします。

旧バージョンといってもそこまで昔のものではないので、特にこだわりがなければこちらの方法で大丈夫なはず。早速見ていきましょう。

インストール手順

1. はじめに、SSReflectとMathCompが対応しているCoq 8.8.0のインストーラを以下のページからダウンロードします。

   Release Coq 8.8.0

   「Assets」の部分から対応するインストーラを選んでダウンロードしてください。32bitの場合はi686、64bitの場合はx86_64を選びます。
2. インストーラをクリックし、セットアップを開始します。
3. 設定はデフォルトのままで構いません。「Next」を押して進んでいきます。
4. インストールが終了すると、スタートメニューにCoqが追加されます。「CoqIde」をクリックしてみてください。画像のようにCoqIdeの画面が表示されていればOKです。
5. 次に、MathComp 1.7.0のインストーラを以下のページからダウンロードします。

   Release The Mathematical Components library 1.7.0

   SSReflectとMathCompはセットになっています。Coqと同様に対応するインストーラを選び、ダウンロードしてください。

6. インストーラをクリックし、セットアップを開始します。
   セットアップ画面に書かれている内容：
   SSReflectとMathCompのインストールを行います。
   セットアップを始める前に他のすべてのアプリケーションを閉じることをおすすめします。これにより再起動することなく関連システムファイルをアップデートできます。
7. こちらも設定はデフォルトのままで大丈夫です。「Next」を押して進んでいきます。
8. インストールが終了したら、CoqIdeを起動して動作を確認します。本のp.27のコードを入れて動かしてみました。

   SSReflect, MathCompも問題なく読み込まれ、正常に動作していることが確認できました。

方法2：WSLでOPAMを利用する

WSL（Windows Subsystem for Linux）でOPAMを利用してインストールします。方法1と比べて少し手間はかかりますが、最新のCoq/SSReflect/MathCompを使うことができます。

WSLのインストールについては以下の記事が分かりやすいのでおすすめです。

こちらの方法ではGUI版のCoqIdeを利用できないので、EmacsをCoqIde代わりにします。普段からLinuxを使っている人や、Emacsが好きな人にはおすすめです。

インストール手順

1. まず、Emacsその他をGUIで使いたいのでVcXsrvをインストールします。

   下のリンクからVcXsrvをダウンロードし、インストールしてください。インストールの際、設定は（たぶん）デフォルトのままで大丈夫です。

   VcXsrv Windows X Server

   インストール後、emacs &やxeyes &でアプリケーションがGUI表示になっていることを確認します。

2. OPAMをインストールします。以下のコマンドを順に実行してください。

   $ sudo add-apt-repository ppa:avsm/ppa

   レポジトリの追加。

   $ opam init -y --disable-sandboxing

   opam initの実行。

   $ opam switch list-available ocaml-base-compiler

   利用可能なスイッチ（コンパイラ）の一覧を表示。

   $ opam switch create X.XX.X

   X.XX.Xには、先ほど一覧表示したスイッチの最新版を指定してください（執筆当時は4.14.0）。処理には時間がかかるので気長に待ちましょう。

   $ eval $(opam env)

   環境変数の設定。

   スイッチの作成opam swith createでエラーが出たときは、ファイル.opamを削除し、再度上記のコードを実行してみてください。

3. Coqをインストールします。

   $ opam install coq

   ※処理には時間がかかります。

   Coqのリリース一覧確認はopam list coqでできます。

4. SSReflect-MathCompをインストールします。

   $ opam repo add coq-released https://coq.inria.fr/opam/released

   レポジトリの追加。

   $ opam list coq-mathcomp-ssreflect

   SSReflect-MathCompのバージョン確認。

   opam install coq-mathcomp-ssreflect.X.XX.X

   最新版のダウンロード（執筆当時は1.14.0）。
5. Emacsの設定を行います。Proof Generalの解説手順にしたがって行います。

   Proof Generalは証明支援器用のEmacs拡張インタフェースです。Proof Generalを導入することにより、EmacsをCoqIdeのようなツールとして使えるようになります。

   Emacsを起動後~/.emacs.d/init.elを開き（無ければinit.elを新規作成）、以下のコードを追加します。

   (require 'package)
   ;; (setq gnutls-algorithm-priority "NORMAL:-VERS-TLS1.3") ; see remark below
   (add-to-list 'package-archives '("melpa" . "https://melpa.org/packages/") t)
   (package-initialize)

   コードを追加したら保存し、Emacsを終了します。

   Emacsを再度起動し、ミニバッファから以下のコマンドを実行してProof Generalをインストールします。

   M-x package-refresh-contents RET

   M-xは「Escキーを押した後にxキーを押す」、RETは「Enterキーを押す」です。

   M-x package-install RET

   proof-general RET

6. 動作確認をします。以下のコードを実行してください。

   $ mkdir Coq
   $ cd Coq
   $ touch test.v

   .vがCoqファイルです。

   Emacsでtest.vを開き、Proof Generalの画面が表示されればOKです！

   軍服を着た女の子はProof Generalイメージキャラクターの「じぇねらるたん」。可愛らしいですね。

   方法1と同じく、実際にコードを入れて動かしてみました。

   こちらも正常に動作していることが確認できました。

トラブルシューティング

Coqをインストールしたはずなのにエラーが出る

Coqを実行しようとして「Searching for Program： そのようなファイルやディレクトリはありません, coqtop」等のエラーが出た場合、OPAMの環境変数の設定が上手く適用されていない可能性があります。

$ eval $(opam env)

インストールされたCoqが正しく認識されているかどうかは、以下のコマンドを実行して確認してみてください。正常に認識されている場合、それぞれのパスが表示されるはずです。

$ which coqc
$ which coqtop
$ which coqidetop.opt

参考記事

インストールにあたり、以下の記事を参考にさせていただきました。

• Installation of MathComp on Windows 10
• Ubuntu 20.04 LTSへのCoq/SSReflect/MathCompのインストールメモ
• 2019年度「プログラミング言語」配布資料

あとがき

最初はSSReflectとMathCompのインストーラはないものと思い込んでいて真っ先にWSLへインストールしたのですが、後から調べてインストーラがあったことを知り、ガッカリしたような嬉しいような…なんだか複雑な気持ちになりました。

何はともあれ、無事にインストールできて一安心です。