Coq/SSReflect/MathCompの設定

Table of Contents

github版

1 設定成功報告

  • [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の場合, バイナリが用意されています(近い将来に Coq platform に頼れ ると期待します). ソースコードからコンパイルすることは手間がかかります.

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を設定([2020-11-09 Mon]時点、Debian系のOS上のバージョン2.0.7 )します:
    • 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 からsourceしなくていいです
      • コンパイラを指定できます; 例えば, opam init --comp=4.11.0
      • eval $(opam env) で設定が完了します
    • opamは既に設定された場合, 最新のパッケージの情報を取得: opam update
    • 使えるパッケージのリスト: opam list -a
  • 次に, OCamlの環境を設定します:
    • opam switch 4.11.1
      • 初めての設定なら, opam switch create 4.11.1
        • opam switch list-available で可能な選択肢が分かります
        • opam switch list ですでに用意されているOCamlのコンパイラを選べます

    - [2020-11-09 Mon]時点, 4.12.0は最新です

  • eval `opam config env` また eval $(opam env)
    • opam switch を行った後, 必要です
  • 次にCoqに必要なOCamlのプログラムを設定します(個人の環境の整備によって, 他のプログラムを設定する必要があるかもしれませんが, opamが教えます):
    • opam update で最新バージョンの情報を取得します
    • opam install camlp5 ([2020-11-09 Mon]時点, 8.00 alpha06は最新です)
      • conf-perl に依存します
    • opam install ocamlfind ([2020-11-09 Mon]時点, 1.8.1は最新です)
      • conf-m4 に依存します
    • opam install num ([2020-11-09 Mon]時点, 1.3は最新です; 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.12.0 ([2020-11-09 Mon]時点, 最新版)
      • conf-findutils に依存します
      • 必要なら, 最新のCoqIDEも設定できます: opam install coqide (10つ以上の依存するライブラリも設定されます)
      • Debian/Ubuntuで 新しいライブラリの設定が要るかもしれません: libgtksourceview-3.0-dev, libgtk-3-dev, libexpat1-dev, libcairo2-dev (など?) (pkg-config は要らなくなりましたか?)
  • 最後に, MathCompを設定します:
    • opam install coq-mathcomp-ssreflect.1.11.0
    • その他のMathCompのパッケージ(prefixは coq-mathcomp です, バージョン1.8.0):
      • 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.12.0 (例えば) で済みます. 要らなくなったパッケージは opam remove coq-mathcomp-odd-order (例えば)で消せます. 問題が生じる場合, opam reinstall coq もできます.

opamとCoqに関する追加情報:

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

コンパイルのために必要なソフトウェアは通常のシステムで既にあるオープンソースソフトウェアです. 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の設定は長い歴史の問題があります.

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

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

2.2.1 事前準備

  1. 方法1・方法2: 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. 方法3: WSLの設定
    • Windowsのバージョンを確認します: Windows Key + R を入力し, winver を実行します (ref).
      • 必要であれば1903以降のバージョンにアップデートします
    • WSL本体と好きなLinuxディストリビューションをインストールします (ref):
      1. 管理者としてWindows PowerShellを起動
      2. Enable-WindowsOptionalFeature -Online -FeatureName Microsoft-Windows-Subsystem-Linux を実行します
      3. 再起動します
      4. Microsoft Storeから, Linuxのディストリビューションをダウンロード・設定します
        • Debian GNU/Linuxは広く使われています. Linux初心者の方にはUbuntu 18.04をおすすめします
    • スタートメニューまたはWindowsの検索窓からLinuxを起動します
      1. ユーザー名とパスワードを入力します
      2. パッケージマネージャーを使って, 基本的なソフトウェアをインストールします:
        • Ubuntu 18.04の場合には sudo add-apt-repository ppa:avsm/ppa を実行します
        • sudo apt update
        • sudo apt-get install emacs
    • WSL上でemacsを使いたいなら, Xorgサーバーは便利でしょう
      1. VcXsrvをダウンロードして, インストールします
      2. XLaunch アイコンでVcXsrvを起動します
      3. multiple windowsstart no client を選びます
    • WSLのshellで DISPLAY という環境変数の設定も必要です: export DISPLAY=localhost:0.0
      • .bashrc にそのコマンドを追加できます (Ubuntu 18.04で確認済み)
      • VcXsrvを起動して, bashを再起動するとX上emacsが使えます

2.2.2 方法1 (cygwin + バイナリ)

  1. Coqを設定
    • releaseページから coq-8.9.1-installer-windows-x86_64.exe を ダウンロードと実行します.
      • ~C:\Coq~として, Coqに関するバイナリを加えられます
    • PATH/cygdrive/c/coq/bin を加えます
      • 例えば, .bashrc に追加 export PATH=${PATH}:/cygdrive/c/coq/bin/ を追加します.
  2. MathCompをソースコードからのコンパイルします

    coqc, coq_makefile などがあれば, 普段通りCoqのライブラリのコンパイルができます.

    • Coqのバイナリでは配布されているMathCompは最新ではないかもしれません.
      • rm /cygdrive/c/coq/lib/user_contrib/mathcomp
    • MathComp 1.9.0を設定するには
      • source files をダウンロードします
      • unzip, untar, cd, make, make installを用いて設定します.
      • 結果で, user-contrib のCoqディレクトーリでMathCompのライブラリなどが追加されます.

2.2.3 方法2 (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.2.4 方法3 (WSL + opam)

  • WSLディストリビューションのパッケージマネージャーを使って, opamをインストールします:
    1. sudo apt install opam
    2. opam init --disable-sandboxing (近い将来 --disable-sandboxing は要らなくなるそうです)
      • 時間がかかります.
    3. opam switch create 4.08.1
      • 時間がかかります.
    4. Debianに基づくディストリビューション以外の場合にはopamのウェブサイトを参照.
  • opam install coq
    • 現時点最[2019-09-24 Tue]新版8.9.1
    • 時間がかかります.
    • 開発版の設定には ([2019-09-24 Tue]):
      • opam repo add coq-core-dev https://coq.inria.fr/opam/core-dev
      • opam install coq.8.10+beta3
  • CoqIDEを使いたいなら, GTK+のヘッダファイルが必要です.
    • sudo apt install libgtk2.0-dev libexpat1-dev (Ubuntu 18.04, Debian 10で確認済み)
      • あるいは sudo apt install libgtk-3-dev libgtksourceview-3.0-dev libexpat1-dev
    • opam install coqide
      • あるいは opam install coqide.8.10+beta3
  • MathCompを設定します
    • opam repo add coq-released https://coq.inria.fr/opam/released
    • opam install coq-mathcomp-ssreflect, etc.

2.2.5 過去の設定報告メモ(参考のため)

  • [2017-01-12 Thu] にcygwin64が flexdll 0.35を含みます. mingw64のパッケージが mingw64-x86_64-xxx となりました.
  • Coq 8.5beta2で成功しましたが, math-compのMakefileが正しくファイルの依存関係を理解しません([2015-10-28 Wed]の時点).
  • Windows 8.1 + cygwin64上でcoq-8.5beta1, ssreflect-1.5.coq85beta1/mathcomp-1.5.coq85beta1Coq 8.5beta1のコンパイル成功しました.
    • 主な問題: 現在[2015-04-04 Sat]のcygwin64のOCamlは動的リンクライブラリをサポートしないため, flexdllからの再コンパイルが必要です.
      • flexdll のソースコードをダウンロードします(現時点の最新版:0.34). 一時的にcygwin64のOCamlパッケージを設定し, mingw64_x86_64-{binutils,gcc-core,runtime}~等も設定します. flexlink.exe等を得るために, ~make demo_mingw64 を行います. 成功したら, cygwin64のOCamlパッケージを外し, PATH に作業ディレクトリを追加します.
      • cygwin64のOCamlパッケージを外して, ソースからコンパイルします.
    • その他の問題:
      • Camlp5の設定: ./configure; make world; make install は成功しますが, なぜか gramlib.a を手動で /cygdrive/c/ocamlmgw64/lib/camlp5 までコピーしなければなりません.
      • MathComp-1.5の設定: mathcomp-1.5.coq85beta1.tar.gzmake が成功しますが, Error: Could not compile the library to native codeが発生します. make install は完成します.
    • 過去にCoqのコンパイルの問題について. 基本的に, Makefileの混乱の問題です: PATH の中にスペースのありなし, PATH の書方の混乱(Unix風とWindows風の混在, .emacs でも), make のバージョンの勘違い, configure のオプション(-arch で無理に linux を指定する必要なことがある), 動的ライブラリの作成関係(しかたがなく, pluginを諦めて, staticなssrcoqのコンパイル, その際SSReflectのmakeのオプションを換ることがあります: make COQC="ssrcoq -coqlib xxx/coq8.4pl4 -q -I ssreflect/v8.4/src -R theories Ssreflect -compile" COQFLAGS=). 等の問題.
  • WindowsでバイナリからCoq/SSReflectを設定するのは一番簡単な方法です. Coq 8.5とMathComp 1.6の設定成功報告[2016-02-01 Mon]
    • 設定済みのCoqの更新なら, コントロールパネルでプログラムアンインス トールをします.
    • Coqのサイトから, coq-installer-8.5-win64.exe をダウンロードし, 実 行します. (Coq files for plugin developersというオプションをわざわ ざ外さなくても良いです.) c:\coq で必要なバイナリ等が置かれます. CoqIdeをメニューから実行できます.
    • MathCompのサイトから, Windows 64 bits installer for Coq 8.5 (ssreflect-mathcomp-installer-1.6-win64.exe )をダウンロードし, 実 行します.
    • c:\coq で必要なファイルが置かれます. メニューからCoqIdeを実行し, From mathcomp Require Import ssreflect. でMathCompの正しい設定を確 認します.
  1. [ALTERNATIVE] ソースからのOCamlの設定

    Windows 8.1 + cygwin64上でOCaml 4.02.1(4.04.0も)のコンパイル成功したことがある. インストールディレクトリで次の作業を行います:

    • cp config/m-nt.h config/m.h
    • cp config/s-nt.h config/s.h
    • cp config/Mafefile.mingw64 config/Makefile
    • make -f Makefile.nt world
    • make -f Makefile.nt install バイナリ等は /cygdrive/c/ocamlmgw64/ に置かれます. /cygdrive/c/ocamlmgw64/bin/PATH に追加します.

    その後, ソースから, Coqなどの設定ができます.

  2. [ALTERNATIVE] ソースコードのアーカイブ・githubからのCoqをのコンパイル

    OCamlやcamlp5等を設定してたら, CoqのソースコードのアーカイブとgithubのMathCompの設定もできます. Windows 10で configure によると([2018-03-08 Thu]):

    Architecture: win32
    Operating system: Windows_NT
    OS dependent libraries: -cclib -lunix
    OCaml version: 4.04.0
    Camlp5 version: 7.03
    Native dynamic link support: true
    

2.3 MacOSの場合

opam を使えると聞きました. Homebrew も使えます(https://github.com/coq/coq/wiki/Installation-of-Coq-on-Mac).

2.4 その他の設定方法

  • Linuxの仮想機械(例えば, VirtualBox)で作業することは時々聞きますが, 仮想機械のfreezeは目撃したことがあります. Coqのwiki で詳細な情報があります.
  • MathLibreのDVDにCoqとSSReflectとMathCompが入っています.
  • SSReflect/MathCompの古いバージョン (http://ssr.msr-inria.inria.fr/FTP にありましたが、消えました)
  • 原将己によるのバイナリ(Coq8.4pl5まで). 次の手順で設定できます. Coqのダウンロードページから coq-installer-8.4pl5.exe ([2017-11-28 Tue]時点, https://coq.inria.fr/download から見つからなってきました) を ダウンロード・インストールし, そして 原将己のページから ssreflect-windows-1.5-8.4pl5mathcomp-windows-1.5-8.4pl5 をダウンロードし, 適切にコピーします.

3 Proof Generalの設定

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

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

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

  • .emacs に次のコードを加えます:
(require 'package)
(let* ((no-ssl (and (memq system-type '(windows-nt ms-dos))
		    (not (gnutls-available-p))))
       (proto (if no-ssl "http" "https")))
  (add-to-list 'package-archives
	       (cons "melpa" (concat proto "://melpa.org/packages/")) t))
(package-initialize)
  • emacs にて:
    • M-x package-refresh-contents RET
    • M-x package-install RET proof-general RET

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

emacsで tt.v という空のファイルを開いてみて, Proof Generalが機動するかどうかを確認します. From mathcomp Require Import eqtype. が通れば, 問題ないでしょう.

4 追加情報

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

ssreflectインストール方法まとめ(Windowsもあるよ!), みずぴー日記

Author: Reynald Affeldt

Created: 2020-11-09 Mon 16:26

Validate