Coq/SSReflect/MathCompの設定

2.1.1. パッケージからの設定

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.926 [2019-11-27 Wed])をダウンロードして, 実行します.
     • 最低限として, 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)))))