Coq/SSReflect/MathCompの設定

Table of Contents

github版

1 設定成功報告

  • [2021-04-12 Mon]: Windows 10 Home, Coq 8.13.2, MathComp 1.12 (WSL 2)
  • [2020-11-20 Fri]: Debian 10.6, Coq 8.12.1 (opam), MathComp 1.11.0 (opam)
  • [2020-11-09 Mon]: Ubuntu 20.04.1 LTS, Coq github master, MathComp github master
  • [2020-08-18 Tue]: Ubuntu 20.04.1 LTS, Coq 8.12.0 (opam), MathComp 1.11.0 (opam)
  • [2019-09-24 Tue]: Windows 10, Coq 8.10beta3 (WSL)
  • [2019-07-12 Fri]: Windows 10, Coq 8.9.1 (opam), MathComp 1.9.0 (opam)
  • [2019-07-08 Mon]: Windows 10, Coq 8.9.1 (binary), MathComp 1.9.0 (source)
  • [2019-05-30 Thu]: Debian 9.7, OCaml 4.06.1, Coq 8.9.1, MathComp 1.9.0 (source)
  • [2019-04-16 Tue]: Debian 9.8, OCaml 4.07.1, Coq 8.9.0 (opam)
  • [2019-04-09 Tue]: Debian 9.7, OCaml 4.06.1, Coq 8.9.0, MathComp-1.8.0 (source)
  • [2018-10-02 Tue]: Debian 9.5, OCaml 4.06.1, Coq 8.8.2 (source), MathComp (github); Windows 10, OCaml 4.04.0 (opam), Coq 8.8.2 (source), MathComp (gitjhub)
  • [2018-08-07 Tue]: Debian 9.5, OCaml 4.06.0, Coq 8.8.1 (source), MathComp(github); Windows 10, OCaml 4.04.0 (opam), Coq 8.8.1 (source), MathComp (github)
  • [2018-04-25 Wed]: Debian 9.4, OCaml 4.04.2, Coq 8.8.0 (source), MathComp (github)
  • [2018-03-08 Thu]: Windows 10, OCaml 4.04.0 (opam), Coq 8.7.2 (source), MathComp (github); Debian 9.3, OCaml 4.04.2, Coq 8.7.2 (source), MathComp (github)
  • [2018-01-16 Tue]: Windows 10, OCaml 4.04.0 (opam), Coq 8.7.1 (source), MathComp (github)
  • [2017-11-28 Tue]: Windows 10, OCaml (opam), Coq 8.7.0 (source), MathComp (github)
  • [2017-10-24 Tue]: Debian 9.1, Coq 8.7.0 (source), MathComp (github); Debian, Coq 8.7.0 (opam), MathComp 1.6.2 (opam)
  • [2017-09-29 Fri]: Debian 9.1, Coq 8.7-beta1 (source), MathComp (github); Debian, Coq 8.6.1 (opam), MathComp 1.6.1 (opam)
  • [2017-07-26 Wed]: Debian 9.1, Coq 8.6.1 (source), MathComp (github)
  • [2017-01-12 Thu]: Windows 8.1, Coq (opam)
  • [2017-01-06 Fri]: Debian 8.6, (opam)
  • [2016-12-21 Wed]: Debian 8.6 / Ubuntu 16.04.1 LTS, OCaml 4.04.0 (opam), Coq 8.6 (source/github), MathComp 1.6.1 (source/github)
  • [2016-02-01 Mon]: Windows 8.1, Coq 8.5, MathComp 1.6 (binary); Ubuntu Server 14.04.1 LTS, (source)
  • [2015-10-30 Fri]: (github)
  • [2015-09-07 Mon]: Debian 8.0, (opam)
  • [2015-06-08 Mon]: Windows 8.1 cygwin64, coq-installer-8.5beta2.exe, ssreflectmathcomp-1.5.coq85beta2.exe
  • [2015-04-04 Sat]: Windows 8.1 cygwin64, ssreflectmathcomp-1.5.coq85beta1
  • [2014-11-19 Wed]: Ubuntu Server 14.04.1 LTS, OCaml 4.01.0, camlp5 6.11, Coq 8.4pl5, SSReflect 1.5, MathComp 1.5

2 Coq/SSReflect/MathCompの設定

設定はUnix系のオペレーティングシステムでスムーズです. ただし, Linuxの パッケージマネージャー(Debianのapt等)のバージョンはいつも遅れています ので, 勧められません. 使える設定方法は2つあります. opamによる設定は 簡単ですが, opamの理解が少し要ります. 最新のパッケージが出来上がるまで に時間はあまりかかりません. トラブルはあまりありません. ソースコードか らコンパイルすることもスムーズです. 最新版を設定する方法として勧めます (リーリスされいないライブラリ(githubのmasterなど)を使いたいとき).

Windowsの場合, バイナリが用意されています. ソースコードからコンパイルすることは手間がかかります.

2.1 Unix系のオペレーティングシステムの場合

2.1.1 パッケージからの設定

OCamlの専用パッケージマネージャー opam でCoqのパッケージを設定ができます. Debianのaptほど遅れていません. SSReflectとMathCompを含むCoqライブラリが用意されています(Coq OPAM packages). 現時点[2020-11-09 Mon], opam show coq-mathcomp-ssreflect によると, 1.11.0版のパッケージがあります.

  • 最初に, opamを設定します:
    • opamをダウンロードします
      • オペレーティングシステムのパッケージマネージャーを使います(例えば, sudo apt get install opam). [2021-04-12 Mon] 時点、Debian系のOS上のバージョンは2.0.3以上ですので, 大丈夫でしょう.
      • あるいは, sh <(curl -sL https://raw.githubusercontent.com/ocaml/opam/master/shell/install.sh)
        • superuserの権利が要るかもしれません
        • /usr/local/bin にインストールされます
    • opam init
      • make, m4, gcc, bubblewrap が要ります
      • /.profile が更新されます
        • 次のログイン, 反映されます(.bashrc から同じ更新しなくてもいいでしょう)
      • コンパイラを指定できます; 例えば, opam init --comp=4.11.2
      • eval $(opam env) で設定が完了します
    • opamは既に設定された場合, 最新のパッケージの情報を取得: opam update
    • 使えるパッケージのリスト: opam list -a
  • 次に, OCamlの環境を設定します:
    • opam switch 4.11.2
      • 初めての設定なら, opam switch create 4.11.2
        • opam switch list-available で可能な選択肢が分かります
        • opam switch list ですでに用意されているOCamlのコンパイラを選べます

    - [2021-04-12 Mon] 時点, 4.13.0は最新です

  • eval `opam config env` また eval $(opam env)
    • opam switch を行った後, 必要です
  • 次にCoqに必要なOCamlのプログラムを設定します(個人の環境の整備によって, 他のプログラムを設定する必要があるかもしれませんが, opamが教えます):
    • opam update で最新バージョンの情報を取得します
    • opam install ocamlfind ([2021-04-12 Mon]時点, 1.9.1は最新です)
    • opam install num ([2021-04-12 Mon]時点, 1.4は最新です; Ocaml 4.06.0から必要です)
  • 次に, Coqを設定します:
    • Coqのリポジトリを追加: opam repo add coq-released https://coq.inria.fr/opam/released
      • opam repo add coq-released --set-default を行うと、これから新しい switch を作ると、Coqのリポジトリを自動的に追加されます
      • Coqのopamパッケージ (prefixは coq- です)
      • opam repo でリポジトリをリストアップできます
    • opam install coq.8.13.2 ([2021-04-12 Mon]時点, 最新版)
      • conf-findutils, conf-gmp, zarith に依存します
        • Debian/Ubuntuで 新しいライブラリの設定が要るかもしれません: libgmp-dev
  • 最後に, MathCompを設定します:
    • opam install coq-mathcomp-ssreflect.1.12.0
    • その他のMathCompのパッケージ(prefixは coq-mathcomp です):
      • coq-mathcomp-fingroup
      • coq-mathcomp-algebra
      • coq-mathcomp-solvable
      • coq-mathcomp-field
      • coq-mathcomp-character
      • coq-mathcomp-finmap
      • coq-mathcomp-bigenough
      • coq-mathcomp-sum-of-two-square, coq-mathcomp-multinomials (user contrib)
      • coq-mathcomp-odd-order (先端な応用ですので, 要らないかもしれません)
  • 今度の更新は, opam update , opam upgrade coq.8.13.2 (例えば) で済みます. 要らなくなったパッケージは opam remove coq-mathcomp-odd-order (例えば)で消せます. 問題が生じる場合, opam reinstall coq もできます.

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

コンパイルのために必要なソフトウェアは通常のシステムで既にあるオープンソースソフトウェアです. Unix系なら, パッケージマネージャーから得られます. 必要なソフトウェアの情報のまとめ:

  • GNU make (バージョン >= 3.81)
  • C compiler
  • TeX/LaTeX (ドキュメントのため)
  • OCaml (バージョン >= 4.05.0; ocaml -version) ([2020-11-09 Mon]時点の最新版: 4.12.0) (インストール)
  • ZArith ([2020-11-09 Mon]時点、最新版: 1.10)
    • インストール: opam install zarith
      • パッケージマネージャーから: libgmp-dev
  • CoqIDEのため: lablgtk3-sourceview3, gtk+3, gtksourceview3
    • インストール: opam install lablgtk3-sourceview3
      • パッケージマネージャーから: libcairo2-dev, libexpat1-dev, libgtk-3-dev, libgtksourceview-3.0-dev
  • Camlp5 (バージョン >= 6.14?; camlp5 -v, 最新版[2020-11-09 Mon]: 8.00, transitionalモード?)
    • 不要になりましたか?
  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-contribmathcomp ディレクトリを削除か名前変更します
    • 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 Windows 10の場合

注意: WindowsでのCoqの設定は長い歴史の問題がありますので, 複数の方法を説明しますが, 設定のために時間があるなら「方法1: WSL 2 + opam」を勧めます. 時間ない場合,「方法2: cygwin + バイナリ」を勧めます.

Windowsで3つの設定方法を説明します:

  • 方法1: WSL 2 + opam (WSL 2でopamを用いてCoqをコンパイルします)
  • 方法2: cygwin + バイナリ (cygwin上Coqのバイナリを使います)
  • 方法3: cygwin + opam (customなopamを用いてCoqをコンパイルします)

2.2.1 事前準備

  1. 方法1: WSL 2 の設定
    • Windowsのバージョンを確認します: Windows Key + R を入力し, winver を実行します (ref).
      • 必要であれば1903以降のバージョンにアップデートします
    • WSL 2本体と好きなLinuxディストリビューションをインストールします (ref):
      1. 管理者としてWindows PowerShellを起動し, 次のコマンドを実行ます: dism.exe /online /enable-feature /featurename:Microsoft-Windows-Subsystem-Linux /all /norestart
      2. 再起動します
      3. 管理者としてWindows PowerShellを起動し, 次のコマンドを実行します: dism.exe /online /enable-feature /featurename:VirtualMachinePlatform /all /norestart
      4. 再起動します
      5. Linux カーネル更新プログラム パッケージをダウンロードし, 実行します.
      6. バーションを設定します: wsl --set-default-version 2
      7. Microsoft Storeから, Linuxのディストリビューションをダウンロード・設定します
        • Debian GNU/Linuxと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・vscodeなどを使うように, Xorgサーバーを設定します:
      1. VcXsrvをダウンロードして, インストールします
      2. XLaunch アイコンでVcXsrvを起動します
      3. multiple windowsstart no clientDisable access control を選び, configurationを保存します
      4. Windows 10の設定を調整します
        • 設定の「ファイアウォールとネットワーク保護」を開きます
        • 「パブリックネットワーク」の下にある「詳細設定」にクリックします
        • 「受信の規則」の「VcXsrv windows xserver」を開きます
        • 「全般」の「操作」を「接続を許可する」にします
        • 「スクープ」に「192.168.0.0/16」を追加します
    • WSLのshellで DISPLAY という環境変数の設定も必要です
      • ./bashrcexport DISPLAY=$(awk '/nameserver / {print $2; exit}' /etc/resolv.conf 2>/dev/null):0 を加えます
  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の設定に関して:
      • .bashrcexport LANG=C が望ましいです.
      • 日本のキーボードを認識できるように, setxkbmap -model jp106 -layout jp を使えます.
      • CAPS LOCKをCTRLにするように, 次の内容を含む Xmodmap ファイルを用意してから, .bashrcxmodmap /home/username/Xmodmap を加えます:
    keycode 66 = Control_L
    clear Lock
    add Control = Control_L
    
    • cygwinに関するその他の情報(例えば, cygwinのアンインストール): cygwin faq

2.2.2 方法1 (WSL 2 + opam)

  • WSL 2の設定が済んでいるなら, 上記の 2.1.1 「パッケージからの設定」と同じ手順になります.

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

2.2.4 [ADVANCED] 方法3 (cygwin + opam)

過去にcygwinのOCamlパッケージの問題はよくあった(ライブラリは足りないこと; flexdll のありなし)し, cygwinで配るopamで設定するOCamlを用いてCoqのコンパイルができなかったので, その2つの方法を使っていません. 代わりに, opamのcustomな設定を用いて, MathCompの設定ができます.

  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.3 MacOSの場合

3 IDEの設定

3.1 IDEの基本的な使い方

  • ショートカット:
  Proof General CoqIDE VSCoq
1つタクティックの実行 CTRL-C CTRL-N CTRL ALT ↓ ALT ↓
1つタクティックのUndo CTRL-C CTRL-U CTRL ALT ↑ ALT ↑
カーソルまでのタクティックの実行 CTRL-C CTRL-ENTER CTRL ALT → ALT →
Check CTRL-C CTRL-A CTRL-C    
Print CTRL-C CTRL-A CTRL-P    
About CTRL-C CTRL-A CTRL-B    
Locate CTRL-C CTRL-A CTRL-L    
Coqをinterrupt CTRL-C CTRL-C    
Coqをkill CTRL-C CTRL-X    

3.2 Proof Generalの設定

インターフェースとして, emacsに慣れているのでしたら, Proof Generalというemacsエディターモードをお勧めします.

  • Unix(WindowsのWSL 2を含む)なら, emacsは必ず入っています.
  • Windowsなら, cygwinで取得できます. Coqを設定すると, CoqIDEという専用インターフェースも設定されます.

Proof Generalの設定に, MELPAとパッケージシステムは進められます:

  • .emacs に次のコードを加えます:
(require 'package)
;; (setq gnutls-algorithm-priority "NORMAL:-VERS-TLS1.3") ; see remark below
(add-to-list 'package-archives '("melpa" . "https://melpa.org/packages/") t)
(package-initialize)
  • emacs にて:
    • M-x package-refresh-contents RET
    • install Proof General
      • M-x package-install RET proof-general RET
      • あるいは, M-x package-list RET, proof-general の行で i を押して, x を押すと, 設定されます.
  • ちゃんと coqtop が見えるターミナルから, emacs tt.v を実行して, From mathcomp Require Import eqtype を書いて, C-c C-n で実行できるかどうか設定の確認できます.

Proof Generalの一番快適な表示はhybridと言い, 次のように設定します:

  • Proof Generalのメニューから, Coq → 3 Windows mode layout → hybrid

Proof Generalを設定したように, company-coq を追加で設定すると, 数学的な記号はきれいに表示されますので, おすすめです。

3.2.1 特別な設定の読み込み

SSReflectとMathCompのバイナリは PATH にない場合, デフォルトな場所で置いていない場合, Coqに教える必要がありますので, 例えば, .emacs に次の変数を設定できます:

(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)))))

一方, coq-prog-args_CoqProject ファイルから読み取ることもできます. 実際に, coq_makefile_CoqProject ファイルを使いますので, その方法のほうが便利です. (_CoqProject の代わりに, 別ファイル名にする場合, emacsで coq-project-filename を設定できます.)

3.3 CoqIDEの設定

伝統的なIDEです. opam を用いて, 設定できます:

  • coq を設定してから, opam install coqide (10つ以上の依存するライブラリも設定されます)
    • Debian/Ubuntuで 新しいライブラリの設定が要るかもしれません: pkg-config, libcairo2-dev, libexpat1-dev, libgtk-3-dev, libgtksourceview-3.0-dev

3.4 vscodeの設定

Visual Studio Code から .deb.rpm をダウンロードし, sudo dpkg -i code_1.55.2-1618307277_amd64.deb ([2021-04-21 Wed]の時点) 設定します. すると, code というエディターを使えます.

Extensions アイコン(あるいはCTRL-SHIFT-X)から, Marketplace から VSCoq ([2021-04-21 Wed]時点: バーション0.3.4) を設定します.

4 追加情報

ソースコードやバイナリのダウンロードのまとめ:

設定に関する追加情報:

Author: Reynald Affeldt

Created: 2021-04-24 Sat 12:56

Validate