Coq/SSReflect/MathCompの設定

2.1.1 パッケージからの設定

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

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

   Coq(SSReflectの一部を含みます)のコンパイル成功報告：

   • ocamlc などを使える状態かを確認します(Unixで $PATH に入っていますか? 例えば, ocamlc -v を試します)
   • Coqをダウンロードします
     • gitで: git clone https://github.com/coq/coq.git
       • git ls-remote --heads
       • trunkブランチからv8.12ブランチに移動: git checkout v8.12
     • または, アーカイブを ダウンロード します
   • できたディレクトリを COQCOMPILEDIRECTORY と呼びます
   • Coqをソースコードからコンパイルします
     • cd coq あるいは cd coq-8.12.0
     • ./configure
       • バイナリのインストールは不要なら, -local を使います
       • バイナリの位置に関して, デフォルト選択で結構です (バイナリは /usr/local/bin, ライブラリは /usr/local/lib/coq 等, superuserになる必要があります)
       • バイナリのインストールの場所を指定するために, -prefix を使います
     • make (ちょっと時間がかかりますので, -jX で並列コンパイルできます)
       • make byte でバイトコード版もできます(デバグに使います)
     • sudo make install
       • -local なら不要 (superuserにならなくいいです)
       • superuserにならないと, デフォルト選択(/usr/local/bin 等)でのインストールが失敗します
       • SSReflectのプラッグインとセオリー(の一部)は COQINSTALLDIRECTORY/plugins/{ssr,ssrmatching,ssrsearch}/ と COQINSTALLDIRECTORY/theories/ssr に置かれます
     • -local の場合以外, make clean できます
     • cd ..
   • coqtop等は使えるようになった状態であるかどうかを確認します
     • export COQBIN=COQINSTALLDIRECTORY/bin/ という変数を作っておいていいです (.bashrc ファイルなら, source .bashrc を行います)
     • 特に, Unixで $PATH に追加します(例えば, export PATH=$COQBIN:$PATH)
   • テスト:

   $ coqtop
   Welcome to machine:directory,master (commit)
   
   Coq < 
   

   MathComp 1.11.0[2020-11-09 Mon]のコンパイル成功報告：

   • 既存のMathCompを削除したほうが無難です
     • COQINSTALLDIRECTORY/user-contrib の mathcomp ディレクトリを削除か名前変更します
   • MathCompのsourcesのソースをダウンロードします
     • git clone https://github.com/math-comp/math-comp.git
       • すでに clone されているなら, git pull --rebase
     • または, アーカイブを ダウンロード します
   • MathCompをコンパイルします:
     • cd math-comp/mathcomp
     • export COQBIN=/COQINSTALLDIRECTORY/bin/ (coqtop等のバイナリがあるディレクトリ)
     • export PATH=$COQBIN:$PATH
     • make (ちょっと時間がかかりますので, -j オプションで並列コンパイルできます)
       • -j オプションで約10分かかります
       • 更新なら, その前, make clean が要るかもしれません
     • sudo make install
       • その結果で, ライブラリは COQINSTALLDIRECTORY/user-contrib/mathcomp に置かれます
       • しないと、明確に示す必要があります
       • localインストールなら, superuserならなくていいです
     • cd ../..
   • coqtop等は使えるようになった状態であるかどうかを確認します. 例えば:

   $ coqtop
   Welcome to machine:directory,master (commit)
   
   Coq < From mathcomp Require Import eqtype.
   [Loading ML file ssrmatching_plugin.cmxs ... done]
   [Loading ML file ssreflect_plugin.cmxs ... done]
   
   Coq < 
   

   さらに, MathComp上のライブラリをソースからコンパイルする場合, 今後そのライブラリの _CoqProject を更新します. 例えば, -R ../math-comp/mathcomp mathcomp の追加によって, ソースからコンパイルしたMathCompを指せます.

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