Coq/SSReflect/MathCompのインストール手順 2022-06-04
Windows10 Home RAM 16GB に 数学定理証明支援システム Coq/SSReflect/MathComp をインストールできたので、その手順を記録公開した。
[参考]
Coq/SSReflect/MathCompの設定 https://staff.aist.go.jp/reynald.affeldt/ssrcoq/install.html
Coq https://coq.github.io/doc/v8.9/refman/index.html
1. WSL (Windows subsystem for Linux) のインストール
[参考]
WSL のインストール https://docs.microsoft.com/ja-jp/windows/wsl/install
WSL の基本的なコマンド https://docs.microsoft.com/ja-jp/windows/wsl/basic-commands
Linux 用 Windows サブシステムで Linux GUI アプリを実行する https://docs.microsoft.com/ja-jp/windows/wsl/tutorials/gui-apps
管理者の PowerShell または Windows コマンド プロンプトで、"wsl --install"
Windowsを再起動
Windows再起動後、自動でUbuntuのインストールが継続もエラー発生
Windowsメニューで、Ubuntuを起動、Ubuntuのインストールが完了、コンソールで Linux Bash が起動
2. WSL の調整
aptパッケージの更新
$ sudo apt update
emacsのインストール
$ sudo apt-get install emacs
3. VcXsrv (X Server for Windows) のインストール
[download from] https://sourceforge.net/projects/vcxsrv/
Windows でインストーラー vcxsrv-64.1.20.14.0.installer を起動
デスクトップのアイコン XLaunch を起動するとオプション選択となる。
multiple windows ・ start no client ・ Disable access control を選び, configurationを保存
とりあえず、private network(初期値on) と public network(初期値off) 両方をon。 )
セキュリティの問題があるため、後で public network を(初期値off)に戻して動作確認は必要。
WSL での DISPLAY環境変数の設定と確認と .bashrc への設定追記
$ export DISPLAY=$(awk ' /nameserver / {print $2; exit}' /etc/resolv.conf 2> /dev/null):0
$ printenv DISPLAY
172.31.160.1:0
"export DISPLAY=$(awk ' /nameserver / {print $2; exit} ' /etc/resolv.conf 2> /dev/null):0"を ".bashrc"へ追記
$ vi .bashrc
(X11 アプリ xcalc, xclock, xeyes をインストールする)
$sudo apt install x11-apps -y
(X11 アプリ xclock を行末の"&"で、バックグランドジョブとして実行することでVcXsrvの動作確認をする)
$xclock &
4. OCamlの専用パッケージマネージャー opam のインストール (WSL で)
$ sudo apt-get install opam
$ opam init
$ eval $(opam env)
$ opam switch list-available
可能な選択肢が表示、最新は 4.13.1 は、自動で選択されていた。
ocaml-base-compiler 4.13.1 Official release 4.13.1
"$ opam switch 4.13.1" をすると選択済と出る。
$ opam update
(Coqに必要なOCamlのプログラムを設定)
$ opam install ocamlfind
$ opam install num
5. Coq をインストール (WSL で)
$ opam repo add coq-released https://coq.inria.fr/opam/released
$ opam repo add coq-released --set-default
(https://github.com/coq/platform/releases/tag/2022.04.0 で Recommended Coq version (最新) Coq 8.15.1 を確認)
$ opam install coq.8.15.1
libgmp-dev がないというエラー発生
$ sudo apt-get install libgmp-dev
$ opam install coq.8.15.1
(https://coq.inria.fr/opam/released/packages/coq-mathcomp-ssreflect/ coq-mathcomp-ssreflect 最新 1.14.0 を確認)
$ opam install coq-mathcomp-ssreflect.1.14.0
$ opam install coq-mathcomp-fingroup.1.14.0
$ opam install coq-mathcomp-algebra.1.14.0
$ opam install coq-mathcomp-solvable.1.14.0
$ opam install coq-mathcomp-field.1.14.0
$ opam install coq-mathcomp-character.1.14.0
$ opam install coq-mathcomp-finmap.1.5.1
$ opam install coq-mathcomp-bigenough.1.0.1
6 CoqIDE をインストール (WSL で)
$ sudo apt-get install pkg-config
$ sudo apt-get install libcairo2-dev libexpat1-dev libgtk-3-dev libgtksourceview-3.0-dev
$ opam install coqide
$ eval $(opam env)
$ sudo apt install yaru-theme-icon
(X11 アプリ coqide を行末の"&"で、バックグランドジョブとして実行する)
$ coqide &
(次回起動用に .bashrc に eval $(opam env) を追加しておくとベター)
