Coq/SSReflect/MathCompの設定

2.1.1 パッケージからの設定

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

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

   Coq 8.9.1[2019-05-21 Tue](SSReflectの一部を含みます)のコンパイル成功報告：

   • ocamlc などを使える状態かを確認します(Unixで $PATH に入っていますか? 例えば, ocamlc -v を試します)
   • COQCOMPILEDIRECTORY というディレクトリでコンパイル作業します
   • Coqをダウンロード します
   • Coqをソースコードからコンパイルします
     • tar xzf coq-8.9.1.tar.gz (coq-8.9.0 というディレクトリは作成されます)
     • cd coq-8.9.1
     • ./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.9.1/bin/ という変数を作っておいていいです (~.bashrc~ファイルなら, ~source .bashrc~を行います)
   • テスト:

   $ coqtop
   Welcome to Coq 8.9.1 (May 2019)
   
   Coq < 
   

   MathComp 1.9.0[2019-05-30 Thu]のコンパイル成功報告：

   • 既存のMathematical Componentsを削除したほうが無難です
     • COQINSTALLDIRECTORY/user-contrib の mathcomp ディレクトリを削除か名前変更します
   • Mathematical Componentsのsources archiveをダウンロード
   • Mathematical Componentsをコンパイルします:
     • tar xzf math-comp-mathcomp-1.9.0.tar.gz
     • cd math-comp-mathcomp-1.9.0/mathcomp
     • export COQBIN=/SOMEWHERE/coq-8.9.1/bin/ (coqtop等のバイナリがあるディレクトリ)
     • make (ちょっと時間がかかりますので, -j オプションで並列コンパイルしてみます)
       • -j オプションで約12分かかります[2019-05-30 Thu]。
     • sudo make install
       • その結果で, ライブラリは COQINSTALLDIRECTORY/user-contrib/mathcomp に置かれます
     • cd ../..
   • coqtop等は使えるようになった状態であるかどうかを確認します. 例えば:

   $ coqtop
   Welcome to Coq 8.9.1 (May 2019)
   
   Coq < From mathcomp Require Import eqtype.
   [Loading ML file ssrmatching_plugin.cmxs ... done]
   [Loading ML file ssreflect_plugin.cmxs ... done]
   
   Coq < 
   

2. [NB: 更新要] githubからのコンパイル
   

   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(?)([2019-01-29 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.9.0/bin/
   • make
     • ちょっと時間がかかります
     • 更新なら, その前, ~make clean~が要るかもしれません
   • make install~　か ~sudo make install
     • COQINSTALLDIRECTORY/coq-8.9.0/user-contrib/mathcomp でバイナリは置かれます.
       • 個人アカウントでバイナリを置くようにした場合, sudo は不要です.
     • SSReflectの一部は COQINSTALLDIRECTORY/coq-8.9.0/plugins/{ssr,ssrmatching}/ にすでにあります.
   • バイナリは通常の場所に置かれていない場合, coqc あるいは coqtop に教える必要があります. ただし, 指定がない場合, COQINSTALLDIRECTORY/coq-8.9.0/user-contrib を見に行きますので, 特別な設定はないかぎりに, -R のオプションは不要になります. それ以外, プラッグインとバイナリが見つかるように, -R COQINSTALLDIRECTORY/coq-8.9.0/user-contrib/mathcomp mathcomp オプションを追加できます.

   $ coqtop 
   Welcome to Coq 8.9.0 (January 2019)
   
   Coq < From mathcomp Require Import eqtype.
   [Loading ML file ssrmatching_plugin.cmxs ... done]
   [Loading ML file ssreflect_plugin.cmxs ... done]
   
   Coq < 
   

2.2.1 事前準備

1. 方法1・方法2: cygwinの設定
   
   • cygwinをインストールするよう, https://www.cygwin.com/から, setup-x86_64.exe (最新版: 2.897 [2019-07-08 Mon])をダウンロードして, 実行します.
     • 最低限として, make, unzip, git, patch, diffutils, emacs, emacs-X11, vim, xinit, texlive のパケージを選びま す.
     • 設定は数分かかります.
   • デスクトップの"Cygwin64 Terminal"アイコンをdouble-clickします.
   • Terminalにて, startxwin を実行して, X11を起動します.
     • そうすると, System Trayアイコンの中に, Cygwin-X11アイコンができるます.
       • みどろの「X」が入っている黒い「C」
     • 右クリックで「システムツール」のメニューからXTermの起動ができます.
       • そうすると, XTermからemacsの実行ができます
   • cygwinの設定に関して:
     • .bashrc に export LANG=C が望ましいです.
     • 日本のキーボードを認識できるように, setxkbmap -model jp106 -layout jp を使えます.
     • CAPS LOCKをCTRLにするように, 次の内容を含む Xmodmap ファイルを用意してから, .bashrc に xmodmap /home/username/Xmodmap を加えます:

   keycode 66 = Control_L
   clear Lock
   add Control = Control_L
   

   • cygwinに関するその他の情報(例えば, cygwinのアンインストール): cygwin faq
2. 方法3: WSLの設定
   
   • Windowsのバージョンを確認します: Windows Key + R を入力し, winver を実行します (ref).
     • 必要であれば1903以降のバージョンにアップデートします
   • WSL本体と好きなLinuxディストリビューションをインストールします (ref):
     1. 管理者としてWindows PowerShellを起動
     2. Enable-WindowsOptionalFeature -Online -FeatureName Microsoft-Windows-Subsystem-Linux を実行します
     3. 再起動します
     4. Microsoft Storeから, Linuxのディストリビューションをダウンロード・設定します
        • Debian GNU/Linuxは広く使われています. Linux初心者の方にはUbuntu 18.04をおすすめします
   • スタートメニューまたはWindowsの検索窓からLinuxを起動します
     1. ユーザー名とパスワードを入力します
     2. パッケージマネージャーを使って, 基本的なソフトウェアをインストールします:
        • Ubuntu 18.04の場合には sudo add-apt-repository ppa:avsm/ppa を実行します
        • sudo apt update
        • sudo apt-get install emacs
   • WSL上でemacsを使いたいなら, Xorgサーバーは便利でしょう
     1. VcXsrvをダウンロードして, インストールします
     2. XLaunch アイコンでVcXsrvを起動します
     3. multiple windows ・ start no client を選びます
   • WSLのshellで DISPLAY という環境変数の設定も必要です: export DISPLAY=localhost:0.0
     • .bashrc にそのコマンドを追加できます (Ubuntu 18.04で確認済み)
     • VcXsrvを起動して, bashを再起動するとX上emacsが使えます

2.2.2 方法1 (cygwin + バイナリ)

1. Coqを設定
   
   • releaseページから coq-8.9.1-installer-windows-x86_64.exe を ダウンロードと実行します.
     • ~C:\Coq~として, Coqに関するバイナリを加えられます
   • PATH に /cygdrive/c/coq/bin を加えます
     • 例えば, .bashrc に追加 export PATH=${PATH}:/cygdrive/c/coq/bin/ を追加します.
2. MathCompをソースコードからのコンパイルします
   

   coqc, coq_makefile などがあれば, 普段通りCoqのライブラリのコンパイルができます.

   • Coqのバイナリでは配布されているMathCompは最新ではないかもしれません.
     • rm /cygdrive/c/coq/lib/user_contrib/mathcomp
   • MathComp 1.9.0を設定するには
     • source files をダウンロードします
     • unzip, untar, cd, make, make installを用いて設定します.
     • 結果で, user-contrib のCoqディレクトーリでMathCompのライブラリなどが追加されます.

2.2.3 方法2 (cygwin + opam)

1. opamによるOCaml等の設定
   

   このページの手動の手順をまとめます:

   • cygwinで次のパケージを設定します:
     • rsync, curl, m4, perl, mingw64-x86_64-gcc-core (or mingw64-i686-gcc-core)
   • opamをダウンロードします.
   • shellで次のコマンドを実行します:
     • tar -xf opam64.tar.xz
     • bash opam64/install.sh
     • opam init default "https://github.com/fdopen/opam-repository-mingw.git#opam2" -c "ocaml-variants.4.07.1+mingw64c" --disable-sandboxing
       • .bash_profile を変更していい
   • eval $(opam config env)
   • opam switch create 4.07.1+mingw64c
     • そのコンパイラーはまだ設定されていないなら
   • opam install camlp5 ([2019-07-12 Fri]'s version: 7.06)
   • opam install ocamlfind ([2019-07-12 Fri]'s version: 1.8.0)
   • conf-m4 も設定されます
   • opam install depext
   • opam install depext-cygwinports ([2019-07-12 Fri]'s version: 0.0.7)
     • その後, /usr/x86_64-w64-mingw32/sys-root/mingw/bin をパスに加える.
   • opam install pcre
     • 成功することがあります；依存するライブラリの一分だけ成功しても大丈夫
   • opam install lablgtk
     • 成功したことはない
     • 基本的なエラー: This package requires gtk+ 2.0 development packages installed on your system
2. opamによるCoqやMathCompの設定
   
   • opam repo add coq-released https://coq.inria.fr/opam/released
   • opam install coq.8.9.1
   • export CAML=/home/username/.opam/4.07.1+mingw64c/bin/
   • export COQBIN=/home/username/.opam/4.07.1+mingw64c/bin/
   • opam install coq-mathcomp-ssreflect
   • opam install coq-mathcomp-fingroup
   • opam install coq-mathcomp-algebra
   • opam install coq-mathcomp-field

2.2.4 方法3 (WSL + opam)

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

1. [ALTERNATIVE] ソースからの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 に追加します.

   その後, ソースから, Coqなどの設定ができます.

2. [ALTERNATIVE] ソースコードのアーカイブ・githubからのCoqをのコンパイル
   

   OCamlやcamlp5等を設定してたら, CoqのソースコードのアーカイブとgithubのMathCompの設定もできます. 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