Ubuntu 20.04 LTSへのCoq/SSReflect/MathCompのインストールメモ

• はじめに
• 参考
• インストール環境
• opamのインストール
• Coqのインストール
• SSReflect-MathCompのインストール
• VSCodeからCoqを使う（2021年5月30日現在、成功せず）
  • VSCodeと拡張機能vscoqのインストール
  • 拡張機能vscoqのインストール（ソースコードから）
  • vscoqの設定
  • 動作確認
  • Windows版CoqIDEとのキーバインド対応
• emacsでProof Generalを使う
  • emacsのインストール
  • Proof Generalのインストール
• 戻る

はじめに_

Coq/SSReflect/MathCompによる定理証明:フリーソフトではじめる数学の形式化で紹介されているCoq/SSReflect/MathCompをUbuntu 20.04 LTS上にインストールした際のメモ

参考_

こちらに従いインストールした。

• Coq/SSReflect/MathCompの設定

インストール環境_

more /etc/os-release 
NAME="Ubuntu"
VERSION="20.04.2 LTS (Focal Fossa)"
ID=ubuntu
ID_LIKE=debian
PRETTY_NAME="Ubuntu 20.04.2 LTS"
VERSION_ID="20.04"
HOME_URL="https://www.ubuntu.com/"
SUPPORT_URL="https://help.ubuntu.com/"
BUG_REPORT_URL="https://bugs.launchpad.net/ubuntu/"
PRIVACY_POLICY_URL="https://www.ubuntu.com/legal/terms-and-policies/privacy-poli
cy"
VERSION_CODENAME=focal
UBUNTU_CODENAME=focal

opamのインストール_

OCamlのパッケージ管理システムopamを使うとインストールが楽とのことなので、まず、こちらからインストールする。

% sudo apt install -y opam

初期化する。設定が~/.bash_profileに追記される。

% opam init
[NOTE] Will configure from built-in defaults.
Checking for available remotes: rsync and local, git, mercurial, darcs. Perfect!

<><> Fetching repository information ><><><><><><><><><><><><><><><><><><><><><>
[default] Initialised

<><> Required setup - please read <><><><><><><><><><><><><><><><><><><><><><><>

  In normal operation, opam only alters files within ~/.opam.

  However, to best integrate with your system, some environment variables
  should be set. If you allow it to, this initialisation step will update
  your bash configuration by adding the following line to ~/.bash_profile:

    test -r /home/gotoh/.opam/opam-init/init.sh && . /home/gotoh/.opam/opam-init/init.sh > /dev/null 2> /dev/null || true

  Otherwise, every time you want to access your opam installation, you will
  need to run:

    eval $(opam env)

  You can always re-run this setup with 'opam init' later.

Do you want opam to modify ~/.bash_profile? [N/y/f]
(default is 'no', use 'f' to choose a different file) y
A hook can be added to opam's init scripts to ensure that the shell remains in
sync with the opam environment when they are loaded. Set that up? [y/N] y

User configuration:
  Updating ~/.bash_profile.
[NOTE] Make sure that ~/.bash_profile is well sourced in your ~/.bashrc.


<><> Creating initial switch (ocaml-system>=4.02.3) <><><><><><><><><><><><><><>

<><> Gathering sources ><><><><><><><><><><><><><><><><><><><><><><><><><><><><>

<><> Processing actions <><><><><><><><><><><><><><><><><><><><><><><><><><><><>
∗ installed base-bigarray.base
∗ installed base-threads.base
∗ installed base-unix.base
∗ installed ocaml-system.4.08.1
∗ installed ocaml-config.1
∗ installed ocaml.4.08.1
Done.
# Run eval $(opam env) to update the current shell environment

以下の記述が~/.bash_profileに追記されていた。

% tail -3 ~/.bash_profile

# opam configuration
test -r /home/gotoh/.opam/opam-init/init.sh && . /home/gotoh/.opam/opam-init/init.sh > /dev/null 2> /dev/null || true

設定を読み込む。

% source ~/.bash_profile
% eval $(opam env)

パッケージリストの更新

% opam update

OCamlをインストール

% opam switch list-available
～中略～
ocaml-base-compiler                    4.12.0
          Official release 4.12.0
ocaml-variants                         4.12.0+options
          Official release of OCaml 4.12.0
ocaml-variants                         4.12.1+trunk
          Latest 4.12 development
ocaml-variants                         4.13.0+trunk
          Current trunk


（2021年5月30日現在、4.13.0が最新版だが、Ubuntuのaptでインストールできるopamのバージョンが古いみたいで、4.13.0がインストールできない。4.12.0をインストールした）
% opam switch create 4.12.0

% opam switch list
#  switch        compiler                    description
→  4.12.0        ocaml-base-compiler.4.12.0  4.12.0
   4.13.0+trunk                              4.13.0+trunk （注：これはインストール失敗したやつ）
   default       ocaml-system.4.08.1         default

（インストールしたOCamlをパスに加える）
% eval $(opam env) 

% which ocaml
/home/gotoh/.opam/4.12.0/bin/ocaml

Coqのインストール_

Coqのインストールに必要なソフトウェアのインストール。

% opam install ocamlfind
% opam install num
% sudo apt install -y libgmp-dev

Coqのリポジトリの追加。

% opam repo add --set-default coq-released https://coq.inria.fr/opam/released

Coqのインストール。最新版をインストールする。

% opam list coq
～中略～
coq.8.13.0       --          Formal proof management system
coq.8.13.1       --          Formal proof management system
coq.8.13.2       --          Formal proof management system

% opam install coq.8.13.2 
～中略～
∗ installed conf-gmp.3
∗ installed zarith.1.12
∗ installed coq.8.13.2
Done.

SSReflect-MathCompのインストール_

% opam list coq-mathcomp-ssreflect
～中略～
coq-mathcomp-ssreflect.1.10.0 --          Small Scale Reflection
coq-mathcomp-ssreflect.1.11.0 --          Small Scale Reflection
coq-mathcomp-ssreflect.1.12.0 --          Small Scale Reflection

% opam install coq-mathcomp-ssreflect.1.12.0
～中略～
∗ installed coq-mathcomp-ssreflect.1.12.0
Done.

私の環境だとUbuntuを起動しなおさないとサーチパスが反映されなかった。以下のコマンドでインストール先が表示されていたら、インストール成功。

% which coqc
/home/gotoh/.opam/4.12.0/bin/coqc

% which coqtop
/home/gotoh/.opam/4.12.0/bin/coqtop

% which coqidetop.opt
/home/gotoh/.opam/4.12.0/bin/coqidetop.opt

% coqc -v
The Coq Proof Assistant, version 8.13.2 (May 2021)
compiled on May 30 2021 10:55:34 with OCaml 4.12.0

VSCodeからCoqを使う（2021年5月30日現在、成功せず）_

VSCodeと拡張機能vscoqのインストール_

• Qiita:@gyu-don Visual Studio CodeでCoqの環境作ってみた
• GitHub: coq-community/vscoq

VSCodeのインストールやUbuntu 20.04との連携は以下のページの「VSCodeのインストール」の項を参照のこと。

• VScodeでWSL上のRuby on Railsコードを書く：VSCodeのインストール

続いて、Ubuntu 20.04 LTS上からVSCodeを起動する。初回は少し時間がかかる。以下の作業ディレクトリの作成は特に意味はない。

% mkdir -p ~/Sandbox/CoqWorkSpace
% cd ~/Sandbox/CoqWorkSpace
% code .

起動したVSCodeにプラグインvscoqをインストールする。

拡張機能vscoqのインストール（ソースコードから）_

2021年5月31日追記：ソースコードから拡張機能を実行したら動いた。

% sudo apt install -y npm
% cd /tmp
% git clone https://github.com/coq-community/vscoq.git
% cd vscoq
% sudo npm i -g vsce
% make |& tee make.log
% ls *vsix
vscoq-0.3.4.vsix （このファイルができていたらコンパイル成功）

（一度、Ubuntu 20.04 LTSとをリモート接続しておく。VSCodeが開いたら終了する）
% code .  

% code --install-extension vscoq-0.3.4.vsix 
Installing extensions...
Extension 'vscoq-0.3.4.vsix' was successfully installed.

(VSCodeを起動し、vscoqが追加されたことを確認する）
% code .

vscoqの設定_

VSCode上で以下の手順で設定する。

1. F1を押す
2. 入力ウィンドウが開くので「settings」と入力し、Enterキーを押す。すると設定画面が開く
3. 「リモート」タブの「Coqtop: Bin Path」の欄にcoqtopのインストール先ディレクトリのパスを入力する。
   • Ubuntuのターミナル上でcoqtopのインストール先ディレクトリを調べる。

     % which coqtop
     /home/gotoh/.opam/4.12.0/bin/coqtop
     

   • 上記のコマンドの結果を参考に入力する（私の例だと/home/gotoh/.opam/4.12.0/bin/）

動作確認_

動作確認をしてみる。

• VSCodeのメニュー欄から「ファイル」→「新規ファイル」
• 言語の選択で「Coq」を選択
• 「ファイル」→「保存」とすすみ、mp.v という名前で保存する。
• ファイルの中身を以下にする（「Coq/SSReflect/MathCompによる定理証明:フリーソフトではじめる数学の形式化」の p. 27より）

  From mathcomp
      Require Import ssreflect.
  
  Section ModusPonens.
  Variables X Y : Prop.
  
  Hypothesis XtoY_is_true : X -> Y.
  Hypothesis X_is_true : X.
  
  Theorem MP : Y .
  Proof.
      move: X_is_true.
      by [].
  Qed.
  
  End ModusPonens.
  

• 「ファイル」→「保存」

1行目にカーソルを合わせて、Altキー＋down（方向キーの下）を押す。本来はcoqtopが動くようだが、2021年5月30日現在、VSCodeのステータス欄（一番下）に「coqtop is not running.」と表示され、動かない。

2021年5月31日追記：ソースコードからコンパイルしたvscoqではちゃんと動いた。

Windows版CoqIDEとのキーバインド対応_

「Coq/SSReflect/MathCompによる定理証明:フリーソフトではじめる数学の形式化」ではWindows版CoqIDEでの操作が説明されているので、それとvscoqの対応は以下の通り。

操作内容	CoqIDE	vscoq
1行読み込み	当該ボタン	Alt + down
1行リセット	当該ボタン	Alt + up
カーソル位置読み込み	当該ボタン	Alt + right
オール読み込み	当該ボタン	Alt + End
オールリセット	当該ボタン	Alt + Home
Checkコマンド	Shift + Ctrl + c	Ctrl + Alt + c
Printコマンド	Shift + Ctrl + p	Ctrl + Alt + p
Display Notationの切り替え	当該チェックボタン	Shift + Alt + n

なお、vscoqのキーバインドは、F1キーをおしたあとに、入力欄で「Coq:」と入力すると調べることができる。

emacsでProof Generalを使う_

emacsで動くCoqのフロントエンドとしてProof Generalがあるとのこと。

• Proof General
• GitHub: ProofGeneral/PG

emacsのインストール_

• WSL2上のUbuntu20.04でのEmacs

Proof Generalのインストール_

• emacsを起動する

  % emacs &
  

• ~/.emacs.d/init.elを開く
• 「(provide 'init)」の上に以下を追加する。

  ;; proof-general
  (leaf proof-general
    :doc "proof-general"
    :tag "coq-frontend" "emacs>=24.5"
    :url " https://proofgeneral.github.io/"
    :emacs>= 24.5
    :ensure t
    )
  

• 保存する（File→SaveかCtrl-c Ctrl-s）
• emacsを終了する

以下のコマンドを実行する。

% cd ~/.emacs.d
% emacs --batch -f batch-byte-compile init.el

emacsを起動するとproof-generalのインストールが始まる。

% emacs &

インストールに成功すると~/.emacs.d/elpa 以下にProof Generalのファイルがある。なお、数字部分はインストール時期によって異なる場合がある。

% ls -1 ~/.emacs.d/elpa | grep proof
proof-general-20210512.556

動作確認をしてみる。作業ディレクトリを作成する。

% mkdir -p ~/Sandbox/CoqWorkSpace
% cd ~/Sandbox/CoqWorkSpace
% touch mp.v

emacsでmp.vを開く（File→Open Fileか Ctrl-x Ctrl-f）。Proof Generalが表示されればOK.

mp.vの中身を以下のように編集し、保存する（「Coq/SSReflect/MathCompによる定理証明:フリーソフトではじめる数学の形式化」の p. 27より）。

From mathcomp
    Require Import ssreflect.

Section ModusPonens.
Variables X Y : Prop.

Hypothesis XtoY_is_true : X -> Y.
Hypothesis X_is_true : X.

Theorem MP : Y .
Proof.
    move: X_is_true.
    by [].
Qed.

End ModusPonens.

ファイルの先頭行にカーソルを合わせ、メニューの「Next」を押していく。1行ずつ実行結果がでれば、OK.

戻る_

• WSL2を用いたUbuntu環境の構築
• Yuichi Goto's page