Coq/SSReflect/MathCompの設定

2.1.1 Unix系のオペレーティングシステムの場合

2.1.2 Windowsの場合

1. Windowsインストーラ
   

   WindowsでバイナリからCoq/SSReflectを設定するのは一番簡単な方法です. Coq 8.5とMathComp 1.6の設定成功報告[2016-02-01 Mon]：

   • まず, 設定済みのCoqの更新なら, コントロールパネルでプログラムアンインストールをします.
   • Coqのサイトから, coq-installer-8.5-win64.exe をダウンロードし, 実行します. (Coq files for plugin developersというオプションをわざわざ外さなくても良いです.) c:\coq で必要なバイナリ等が置かれます. CoqIdeをメニューから実行できます.
   • MathCompのサイトから, Windows 64 bits installer for Coq 8.5 (ssreflect-mathcomp-installer-1.6-win64.exe )をダウンロードし, 実行します.
   • c:\coq で必要なファイルが置かれます. メニューからCoqIdeを実行し, From mathcomp Require Import ssreflect. でMathCompの正しい設定を確認します.
2. opam
   

   [2017-01-12 Thu]時点, Windowsでもopamを使えるようになりましたが, まだ不安定みたいです.

   • [2015-09-07 Mon]時点: cygwin64でのソースからのコンパイルは失敗しました; cygwin64との相性は悪いみたいです; cygwin32なら, opamはあるそうですが、自分で動作確認しませんでした.

   opamのインストール をそのまま成功します (現時点[2017-01-12 Thu]の最新版は[2016-07-18 Mon]). (手動で, cywginを用いて, opam install depext depext-cygwinports まで確認しました. graphicalインストーラはまだ確認していません.) ただし, opamを設定してから, 上記のopamによるMathCompの設定は完全に通りません:

   • [X] opam install camlp5
   • [X] opam install ocamlfind
   • [X] eval `opam config env`
   • [X] opam repo add coq-released https://coq.inria.fr/opam/released
   • [X] opam install coq.8.6
   • [ ] opam install coqide.8.6 (opam depext conf-pkg-config.1.0 を行っても, pkg-config, libgtksourceview2.0-devel のcygwinを設定しても, missing external dependencies で設定は失敗します.)
   • [ ] opam install coq-mathcomp-ssreflect.1.6.1 (Windowsのpathを読み間違い見たいです.)

   これから, MathCompのソースからのコンパイルはすぐ通らなかったです(検討中).

3. その他
   
   • Linuxの仮想機械(例えば, VirtualBoxで作業することは時々聞きますが, 仮想機械のfreezeは目撃したことがあります.
   • MathLibreのDVDにCoqとSSReflectとMathCompが入っています.
   • 他のSSReflect/MathCompのバイナリ:
     • SSReflect/MathCompの古いバージョン: http://ssr.msr-inria.inria.fr/FTP/.
   • 原将己によるのバイナリ(Coq8.4pl5まで). 次の手順で設定できます. Coqのダウンロードページから coq-installer-8.4pl5.exe を ダウンロード・インストールし, そして 原将己のページから ssreflect-windows-1.5-8.4pl5 と mathcomp-windows-1.5-8.4pl5 をダウンロードし, 適切にコピーします.

2.3.1 Unix系のオペレーティングシステムでのコンパイル

1. githubからのコンパイル
   

   Coq 8.6とSSReflect/MathComp 1.6.1のコンパイル成功報告.

   • Coqをコンパイルします.
     • githubからソースコードを取得します: git clone https://github.com/coq/coq.git
     • cd coq
     • git ls-remote --heads
     • trunkブランチからv8.6ブランチに移動： git checkout v8.6
     • 開発版なので, 設定ディレクトリのままにします： ./configure -local -usecamlp5
     • make world
   • MathCompをコンパイルします. (SSReflectを含みます.)
     • githubからソースコードを取得します： git clone https://github.com/math-comp/math-comp.git
     • cd math-comp/mathcomp
     • 開発版のCoqを見つかるように： export COQBIN=/MYINSTALLDIRECTORY/coq/bin/
     • make
   • バイナリは通常の場所に置かれていないので, coqc あるいは coqtop に教える必要があります （基本的に, -R MYINSTALLDIRECTORY/math-comp/mathcomp mathcomp オプションの追加となります）.

2. ソースコードのアーカイブからコンパイル
   

   Coq 8.6とSSReflect/MathComp 1.6.1[2016-12-21 Wed]のコンパイル成功報告：

   • ocamlc などを使える状態かを確認します(Unixで $PATH に入っていますか? 例えば, ocamlc -v を試します)
   • /MYCOMPILEDIRECTORY というディレクトリでコンパイル作業します
   • Coqをダウンロード します
   • Coqをソースコードからコンパイルします
     • tar xzf coq-8.6.tar.gz (coq-8.6というディレクトリは作成されます)
     • cd coq-8.6
     • ./configure -usecamlp5
       • バイナリの位置に関して, デフォルト選択で結構です (バイナリは /usr/local/bin, ライブラリは /usr/local/lib/coq 等)
       • バイナリのインストールは不要なら, -local を使います
       • バイナリのインストールの場所を指定するために, -prefix を使います
       • lablGtk2を指すために, -lablgtkdir /DIR を使えるそうです
       • LablGtk2を見つからないと, CoqIdeをコンパイルできませんが, Coqをちゃんとコンパイルできます
     • make world (ちょっと時間がかかりますので, -j で並列コンパイルしてみます)
     • sudo make install (superuserにならないと, デフォルト選択(/usr/local/bin 等)でのインストールが失敗します)
     • make clean
     • cd ..

   • coqtop等は使えるようになった状態であるかどうかを確認します (特に, Unixで $PATH に入っていますか?). 例えば:

   $ coqtop
   Welcome to Coq 8.6 (December 2016)
   
   Coq <
   

   • Mathematical Componentsのsources archiveをダウンロード
   • Mathematical Componentsをコンパイルします:
     • tar xzf math-comp-mathcomp-1.6.1.tar.gz
     • cd math-comp-mathcomp-1.6.1
     • export COQBIN=/usr/local/bin/ (coqtop等のバイナリがあるディレクトリ)
     • cd mathcomp
     • make (ちょっと時間がかかりますので, -jオプションで並列コンパイルしてみます)
     • sudo make install (その結果で, ライブラリは /usr/local/lib/coq/user-contrib/mathcomp に置かれます. 1.5版までは /usr/local/lib/coq/user-contrib/Ssreflect と /usr/local/lib/coq/user-contrib/MathComp でした.)
     • cd ../..
   • coqtop等は使えるようになった状態であるかどうかを確認します. 例えば:

   $ coqtop -R /MYINSTALLDIRECTORY/math-comp/mathcomp/ mathcomp
   Welcome to Coq 8.6 (December 2016)
   
   Coq < From mathcomp Require Import ssreflect.
   [Loading ML file ssrmatching_plugin.cmxs ... done]
   
   Small Scale Reflection version 1.6 loaded.
   Copyright 2005-2016 Microsoft Corporation and INRIA.
   Distributed under the terms of the CeCILL-B license.
   
   [Loading ML file ssreflect_plugin.cmxs ... done]
   
   Coq <
   

2.3.2 Windowsでのコンパイル

1. githubからのコンパイル
   

   Windows + Cygwin上でUnix上の設定方法は基本的に通りますが, 相変わらず不思議なことがあります. Coq 8.5beta2で成功しましたが, math-compのMakefileが正しくファイルの依存関係を理解しません（[2015-10-28 Wed]の時点）.

2. ソースコードのアーカイブからコンパイル
   

   NB: [2017-01-12 Thu] にcygwin64が flexdll 0.35を含みます. mingw64のパッケージが mingw64-x86_64-xxx となりました. ただし, 下記のコンパイル方法は再現できませんでした(検討中).

   Windows 8.1 + cygwin64上でOCaml 4.02.1, coq-8.5beta1, ssreflect-1.5.coq85beta1/mathcomp-1.5.coq85beta1Coq 8.5beta1のコンパイル成功報告 (上記の「Unix系のオペレーティングシステムでの設定」も参考になります). 主な問題: 現在[2015-04-04 Sat]のcygwin64のOCamlは動的リンクライブラリをサポートしないため, flexdllからの再コンパイルが必要です.

   • flexdllの設定：flexdll のソースコードをダウンロードします（最新版:0.34）. 一時的にcygwin64のOCamlパッケージを設定し, mingw64_x8664-{binutils,gcc-core,runtime}等も設定します. flexlink.exe等を得るために, make demo_mingw64 を行います. 成功したら, cygwin64のOCamlパッケージを外し, PATH に作業ディレクトリを追加します.
   • Ocaml-4.02.1 (-> 4.04.0) の設定：インストールディレクトリで次の作業を行います:
     • cp config/m-nt.h config/m.h
     • cp config/s-nt.h config/s.h
     • cp config/Mafefile.mingw64 config/Makefile
     • make -f Makefile.nt world
     • make -f Makefile.nt install

     バイナリ等は /cygdrive/c/ocamlmgw64/ に置かれます. /cygdrive/c/ocamlmgw64/bin/ を PATH に追加します.

   • Camlp5の設定： ./configure; make world; make install は成功しますが, なぜか gramlib.a を手動で /cygdrive/c/ocamlmgw64/lib/camlp5 までコピーしなければなりません.
   • Coq-8.5beta1の設定： ./configure -local でコンパイルします.
   • SSReflect-1.5の設定： ssreflect-1.5.coq85beta1.tar.gz を取得します. COQBIN 変数を coqtop 等のディレクトリに設定し, PATH に追加します make; make install は成功します.
   • MathComp-1.5の設定： mathcomp-1.5.coq85beta1.tar.gz を取得します. make が成功しますが, Error: Could not compile the library to native codeが発生します. make install が完成します.