Coq/SSReflect/MathCompの設定

2.1.1 パッケージからの設定

2.1.2 ソースコードからのコンパイル

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

   Coq 8.8.2[2018-10-02 Tue](SSReflectの一部を含みます)のコンパイル成功報告：

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

   • coqtop等は使えるようになった状態であるかどうかを確認します
     • 特に, Unixで $PATH に追加します
     • export COQBIN=COQINSTALLDIRECTORY/coq-8.8.2/bin/ という変数を作っておいていいです (~.bashrc~ファイルなら, ~source .bashrc~を行います)
   • テスト:

   $ coqtop
   Welcome to Coq 8.8.2 (October 2018)
   
   Coq < 
   

   [NB: 更新要] MathComp 1.6.1[2016-12-21 Wed]のコンパイル成功報告：

   • 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 MCINSTALLDIRECTORY/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. githubからのコンパイル
   

   [NB: 更新要] Coq 8.6をコンパイルします.

   • 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 1.7([2018-10-02 Tue]版)をコンパイルします(SSReflectの一部を含みます):

   • githubからソースコードを取得します：
     • git clone https://github.com/math-comp/math-comp.git
     • すでに clone されているなら, git pull --rebase
   • cd math-comp/mathcomp
   • 開発版のCoqを見つかるように： export COQBIN=COQINSTALLDIRECTORY/coq-8.8.2/bin/
   • make
     • ちょっと時間がかかります
     • 更新なら, その前, ~make clean~が要るかもしれません
   • make install~　か ~sudo make install
     • COQINSTALLDIRECTORY/coq-8.8.2/user-contrib/mathcomp でバイナリは置かれます.
       • 個人アカウントでバイナリを置くようにした場合, sudo は不要です.
     • SSReflectの一部は COQINSTALLDIRECTORY/coq-8.8.2/plugins/{ssr,ssrmatching}/ にすでにあります.
   • バイナリは通常の場所に置かれていない場合, coqc あるいは coqtop に教える必要があります. ただし, 指定がない場合, COQINSTALLDIRECTORY/coq-8.8.2/user-contrib を見に行きますので, 特別な設定はないかぎりに, -R のオプションは不要になります. それ以外, プラッグインとバイナリが見つかるように, -R COQINSTALLDIRECTORY/coq-8.8.2/user-contrib/mathcomp mathcomp オプションを追加できます.

   $ coqtop 
   Welcome to Coq 8.8.2 (October 2018)
   
   Coq < From mathcomp Require Import eqtype.
   [Loading ML file ssrmatching_plugin.cmxs ... done]
   [Loading ML file ssreflect_plugin.cmxs ... done]
   
   Coq < 
   

2.2.1 Windowsインストーラ

2.2.2 ソースコードからのコンパイル

1. 準備1: cygwin
   

   ソースから設定すると, Unix系のshellのインターフェスが便利ですので, cygwinの設定を勧めます.

   • cywinをインストールするよう, https://www.cygwin.com/から, setup-x86_64.exe (最新版: 2.9.0 [2017-11-28 Tue])をダウンロードして, 実行します.
   • 最低限として, emacs, xinit, make, texlive のパケージを選びます.
   • .bashrc に export LANG=C が望ましいです.
   • startxwin でX11を起動します. Windowsのタスクバーで見つかるcygwinのアイコンから, 「システムツール」のメニューから xterm 等を起動ができます.
   • cygwinに関するその他の情報(例えば, cygwinのアンインストール): cygwin faq
2. 準備2: OCaml
   
   1. opamによるOCaml等の設定
      

      Windowsでもopamを使えるようになりました([2018-10-02 Tue]). このページの手動の手順をまとめます(graphicalインストーラはまだ確認していません):

      • cygwinで次のパケージを設定します:
        • rsync
        • patch
        • diffutils
        • curl
        • make
        • unzip
        • git
        • m4
        • perl
        • mingw64-x86₆₄-gcc-core (or mingw64-i686-gcc-core)
      • opamをダウンロードします.
      • shellで次のコマンドを実行します:
        • tar -xf opam64.tar.xz
        • bash opam64/install.sh
        • opam init mingw 'https://github.com/fdopen/opam-repository-mingw.git' --comp 4.02.3+mingw64c --switch 4.02.3+mingw64c
          • .bash_profile と .ocamlinit を変更していい
          • その後, opam switch 4.03.0+mingw64c, opam switch 4.04.0+mingw64c ができる
          • ただし, permission denied問題が発生することがあります(特に, 上記以上のバージョンを設定できたことはありません). 原因不明. ディレクトリーのpermissionを緩めて, 管理者としてcygwinを実行して, 実行を繰り返すと成功するもあります. 下記の設定も同じ問題があります.
      • eval $(opam config env)
      • opam install camlp5 ([2018-01-16 Tue]'s version: 7.03)
      • opam install ocamlfind ([2018-01-16 Tue]'s version: 1.7.3-1)
        • conf-m4 も設定されます
      • lablgtkのため
        • opam install depext
          • 成功したことがある
        • opam install depext-cygwinports ([2018-01-16 Tue]'s version: 0.0.6)
          • 成功したことがある
          • その後, /usr/x86_64-w64-mingw32/sys-root/mingw/bin をパスに加える.
        • opam install pcre
          • 成功したことがある
        • opam install lablgtk
          • 成功したことはない

      以上, OCaml等の設定ができますが, opamを用いてCoqの設定は成功したことないです:

      • [X] opam repo add coq-released https://coq.inria.fr/opam/released
      • [ ] opam install coq.8.7.{0,1}
        • num, base, ~base-num~しか設定できたことはない
   2. ソースからのOCamlの設定
      

      Windows 8.1 + cygwin64上で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 に追加します.
   3. cygwinのOCamlについて
      

      過去にcygwinのOCamlパッケージの問題はよくありました(ライブラリは足りないこと; flexdll のありなし)ので, 最近使っていません.

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

   opamでOCamlやcamlp5等を設定してたら, CoqのソースコードのアーカイブとgithubのMathCompの設定が成功しました. Unixの場合と同じ手順ですが, cygwinのせいでコンパイルは遅くなります. Windows 10で configure によると([2018-03-08 Thu]):

   Architecture: win32
   Operating system: Windows_NT
   OS dependent libraries: -cclib -lunix
   OCaml version: 4.04.0
   Camlp5 version: 7.03
   Native dynamic link support: true
   

   過去の設定報告メモ(参考のため):

   • [2017-01-12 Thu] にcygwin64が flexdll 0.35を含みます. mingw64のパッケージが mingw64-x86_64-xxx となりました.
   • Coq 8.5beta2で成功しましたが, math-compのMakefileが正しくファイルの依存関係を理解しません([2015-10-28 Wed]の時点).
   • Windows 8.1 + cygwin64上でcoq-8.5beta1, ssreflect-1.5.coq85beta1/mathcomp-1.5.coq85beta1Coq 8.5beta1のコンパイル成功しました.
     • 主な問題: 現在[2015-04-04 Sat]のcygwin64のOCamlは動的リンクライブラリをサポートしないため, flexdllからの再コンパイルが必要です.
       • flexdll のソースコードをダウンロードします(現時点の最新版:0.34). 一時的にcygwin64のOCamlパッケージを設定し, mingw64_x86_64-{binutils,gcc-core,runtime}~等も設定します. flexlink.exe等を得るために, ~make demo_mingw64 を行います. 成功したら, cygwin64のOCamlパッケージを外し, PATH に作業ディレクトリを追加します.
       • cygwin64のOCamlパッケージを外して, ソースからコンパイルします.
     • その他の問題:
       • Camlp5の設定: ./configure; make world; make install は成功しますが, なぜか gramlib.a を手動で /cygdrive/c/ocamlmgw64/lib/camlp5 までコピーしなければなりません.
       • MathComp-1.5の設定: mathcomp-1.5.coq85beta1.tar.gz で make が成功しますが, Error: Could not compile the library to native codeが発生します. make install は完成します.
     • 過去にCoqのコンパイルの問題について. 基本的に, Makefileの混乱の問題です: PATH の中にスペースのありなし, PATH の書方の混乱(Unix風とWindows風の混在, .emacs でも), make のバージョンの勘違い, configure のオプション(-arch で無理に linux を指定する必要なことがある), 動的ライブラリの作成関係(しかたがなく, pluginを諦めて, staticなssrcoqのコンパイル, その際SSReflectのmakeのオプションを換ることがあります: make COQC="ssrcoq -coqlib xxx/coq8.4pl4 -q -I ssreflect/v8.4/src -R theories Ssreflect -compile" COQFLAGS=). 等の問題.