Coq/SSReflect/MathCompの設定

2.1.1 パッケージからの設定

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

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: WSL 2 の設定
   

   NB: [2022-02-19 Sat] Windows 10 version 2004から(Windows 11を含めて), ~wsl –install~で, virtualizationを設定し、最新のkernelのLinux distributionを設定します.

   • Windowsのバージョンを確認します: Windows Key + R を入力し, winver を実行します (ref).
     • 必要であれば1903以降のバージョンにアップデートします
   • WSL 2本体と好きなLinuxディストリビューションをインストールします (ref):
     1. 管理者としてWindows PowerShellを起動し, 次のコマンドを実行します: wsl --install
     2. 再起動すると、Ubuntuが起動する

   • スタートメニューまたはWindowsの検索窓からLinuxを起動します
     1. ユーザー名とパスワードを入力します
     2. パッケージマネージャーを使って, 基本的なソフトウェアをインストールします:
        • Ubuntu 18.04の場合には sudo add-apt-repository ppa:avsm/ppa を実行します.
        • sudo apt update
        • ~sudo apt-get install
   • *emacs*の場合：
     • WSL 2上でX上のemacsなどを使うように, Xorgサーバーを設定します:
       1. VcXsrvをダウンロードして, インストールします
       2. XLaunch アイコンでVcXsrvを起動します
       3. multiple windows ・ start no client ・ Disable access control を選び, configurationを保存します
       4. Windows 10の設定を調整します
          • 設定の「ファイアウォールとネットワーク保護」を開きます
          • 「パブリックネットワーク」の下にある「詳細設定」にクリックします
          • 「受信の規則」の「VcXsrv windows xserver」を開きます
          • 「全般」の「操作」を「接続を許可する」にします
          • 「スクープ」に「192.168.0.0/16」,「172.17.0.0/16」,「172.18.0.0/16」,「172.19.0.0/16」,…, 「172.26.0.0/16」,「172.27.0.0/16」,「172.28.0.0/16」,「172.27.0.0/16」などを追加します。 実際に、どのアドレスが本当に必要なのか、WSLを起動して echo $DISPLAY で分かります。ただし、よく変わりますので、いくつかを先に登録しておいていいでしょう。
     • WSLのshellで DISPLAY という環境変数の設定も必要です
       • ./bashrc に export DISPLAY=$(awk '/nameserver / {print $2; exit}' /etc/resolv.conf 2>/dev/null):0 を加えます
   • *VSCode*の場合
     1. VSCode(Windows版)をインストールする
     2. 拡張機能で wsl と検索して、Remote - WSL をインストールする
     3. Ubuntuを再起動する
     4. code . を実行すると、VSCodeが開き連動していることが確認できる
     5. 確認できたら、以降の設定は必要なく、2.1.1 「パッケージからの設定」と同じ手順で進める
2. 方法2・方法3: 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.2.2 方法1 (WSL 2 + opam)

2.2.3 方法2 (cygwin + バイナリ)

2.2.4 [ADVANCED] 方法3 (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

3.2.1 特別な設定の読み込み

(setq coq-prog-name "COQINSTALLDIRECTORY/coq-8.7.0/bin/coqtop")
(setq coq-prog-args
  (cons "-R" (cons "COQINSTALLDIRECTORY/coq-8.7.0/user-contrib/mathcomp" (cons "mathcomp" (cons "-emacs" nil)))))