Coq/SSReflect/MathCompのインストール手順

 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) を追加しておくとベター)

追記 2022-06-06

coqide起動後、NVIDIA グラフィックボードのデバイスドライバから、WSLコンソール上に次のエラーが出るが、当面実害はなさそう。

"NVD3D10: CPU cyclestats are disabled on client virtualization" 

調査すると、最新デバイスドライバの提供を待つ必要ありとのこと。