Coq/SSReflect/MathCompの設定

設定成功報告

[2023-02-24 Fri]: Ubuntu 22.04.1 LTS, Coq 8.16.1, MathComp 1.16
[2023-01-06 Fri]: Ubuntu 22.04.1, opam 2.1.4, ocaml 4.14.1, Coq 8.16.1, ProofGeneral 4.6, MathComp 1.15.0, MathComp-Analysys 0.6.0
[2022-09-09 Fri]: Ubuntu 22.04.1, Coq 8.15, MathComp 1.15 (opam), ProofGeneral 4.6
[2022-08-03 Wed]: Windows 11, Coq 8.15, MathComp 1.15 (WSL 2)
[2022-02-29 Sat]: Windows 11 21H2, Coq 8.15, MathComp 1.14 (WSL 2)
[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

Coq/SSReflect/MathCompの設定

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

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

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

パッケージからの設定

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

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

　　　 - [2023-02-24 Fri] 時点, 5.0.0は最新ですが、急いで使う必要はないです

eval `opam config env` また eval $(opam env)
- opam switch を行った後, 必要です
次にCoqに必要なOCamlのプログラムを設定します(個人の環境の整備によって, 他のプログラムを設定する必要があるかもしれませんが, opamが教えます):
- opam update で最新バージョンの情報を取得します
- opam install ocamlfind ([2023-02-24 Fri]時点, 1.9.5は最新です)
- opam install num ([2023-02-24 Fri]時点, 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.16.1 ([2023-02-24 Fri]時点, 最新版)
  - conf-findutils, conf-gmp, zarith, dune に依存します
    - Debian/Ubuntuで新しいライブラリの設定が要るかもしれません: libgmp-dev
最後に, MathCompを設定します:
- opam install coq-mathcomp-ssreflect.1.16.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.16.1 (例えば) で済みます. 要らなくなったパッケージは opam remove coq-mathcomp-odd-order (例えば)で消せます. 問題が生じる場合, opam reinstall coq もできます.

Windows 10 & 11の場合

注意: 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をコンパイルします)

事前準備

方法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・方法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

方法1 (WSL 2 + opam)

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

方法2 (cygwin + バイナリ)

Coq Platformのreleaseページから, バイナリーをダウンロードと実行します.

[ADVANCED] 方法3 (cygwin + opam)

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

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

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

[WIP] MacOSの場合

Coq platform または Homebrew を使えます: https://github.com/coq/coq/wiki/Installation-of-Coq-on-Mac

emacsのインストール：

install macports
PATH=/opt/local/bin:$PATH
sudo port selfupdate
sudo port install emacs-app

IDEの設定

IDEの基本的な使い方

ショートカット:

	Proof General	CoqIDE	VSCoq
１つタクティックの実行	CTRL-C CTRL-N	CTRL ALT ↓	ALT ↓
１つタクティックの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

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 を追加で設定すると, 数学的な記号はきれいに表示されますので, おすすめです。

特別な設定の読み込み

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 を設定できます.)

CoqIDEの設定

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

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

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) を設定します.

追加情報

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

Coq (github, beta版など)
Mathematical Components (github)
Proof General

設定に関する追加情報：

Coqのサイトによるopamの設定方法
MathCompによる設定の説明
MathLibreのDVDにCoqとSSReflectとMathCompが入っています.
Coqのwiki でWindowsに関して詳細な情報があります.

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

install-jp.org

install-jp.org

Coq/SSReflect/MathCompの設定

設定成功報告

Coq/SSReflect/MathCompの設定

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

パッケージからの設定

Windows 10 & 11の場合

事前準備

方法1: WSL 2 の設定

方法2・方法3: cygwinの設定

方法1 (WSL 2 + opam)

方法2 (cygwin + バイナリ)

[ADVANCED] 方法3 (cygwin + opam)

opamによるOCaml等の設定

opamによるCoqやMathCompの設定

[WIP] MacOSの場合

IDEの設定

IDEの基本的な使い方

Proof Generalの設定

特別な設定の読み込み

CoqIDEの設定

vscodeの設定

追加情報

Files

install-jp.org

Latest commit

History

install-jp.org

File metadata and controls

Coq/SSReflect/MathCompの設定

設定成功報告

Coq/SSReflect/MathCompの設定

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

パッケージからの設定

Windows 10 & 11の場合

事前準備

方法1: WSL 2 の設定

方法2・方法3: cygwinの設定

方法1 (WSL 2 + opam)

方法2 (cygwin + バイナリ)

[ADVANCED] 方法3 (cygwin + opam)

opamによるOCaml等の設定

opamによるCoqやMathCompの設定

[WIP] MacOSの場合

IDEの設定

IDEの基本的な使い方

Proof Generalの設定

特別な設定の読み込み

CoqIDEの設定

vscodeの設定

追加情報