Coq/SSReflect/MathCompの設定
Table of Contents
→ github版 ←
1 設定成功報告
- : Ubuntu 20.04.1 LTS, Coq github master, MathComp github master
- : Ubuntu 20.04.1 LTS, Coq 8.12.0 (opam), MathComp 1.11.0 (opam)
- : Windows 10, Coq 8.10beta3 (WSL)
- : Windows 10, Coq 8.9.1 (opam), MathComp 1.9.0 (opam)
- : Windows 10, Coq 8.9.1 (binary), MathComp 1.9.0 (source)
- : Debian 9.7, OCaml 4.06.1, Coq 8.9.1, MathComp 1.9.0 (source)
- : Debian 9.8, OCaml 4.07.1, Coq 8.9.0 (opam)
- : Debian 9.7, OCaml 4.06.1, Coq 8.9.0, MathComp-1.8.0 (source)
- : 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)
- : 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)
- : Debian 9.4, OCaml 4.04.2, Coq 8.8.0 (source), MathComp (github)
- : 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)
- : Windows 10, OCaml 4.04.0 (opam), Coq 8.7.1 (source), MathComp (github)
- : Windows 10, OCaml (opam), Coq 8.7.0 (source), MathComp (github)
- : Debian 9.1, Coq 8.7.0 (source), MathComp (github); Debian, Coq 8.7.0 (opam), MathComp 1.6.2 (opam)
- : Debian 9.1, Coq 8.7-beta1 (source), MathComp (github); Debian, Coq 8.6.1 (opam), MathComp 1.6.1 (opam)
- : Debian 9.1, Coq 8.6.1 (source), MathComp (github)
- : Windows 8.1, Coq (opam)
- : Debian 8.6, (opam)
- : Debian 8.6 / Ubuntu 16.04.1 LTS, OCaml 4.04.0 (opam), Coq 8.6 (source/github), MathComp 1.6.1 (source/github)
- : Windows 8.1, Coq 8.5, MathComp 1.6 (binary); Ubuntu Server 14.04.1 LTS, (source)
- : (github)
- : Debian 8.0, (opam)
- : Windows 8.1 cygwin64, coq-installer-8.5beta2.exe, ssreflectmathcomp-1.5.coq85beta2.exe
- : Windows 8.1 cygwin64, ssreflectmathcomp-1.5.coq85beta1
- : 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).
現時点 , opam show coq-mathcomp-ssreflect
によると,
1.11.0版のパッケージがあります.
- 最初に, opamを設定( 時点、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のコンパイラを選べます
- 初めての設定なら,
-
時点, 4.12.0は最新ですeval `opam config env`
またeval $(opam env)
opam switch
を行った後, 必要です
- 次にCoqに必要なOCamlのプログラムを設定します(個人の環境の整備によって, 他のプログラムを設定する必要があるかもしれませんが, opamが教えます):
opam update
で最新バージョンの情報を取得しますopam install camlp5
( 時点, 8.00 alpha06は最新です)conf-perl
に依存します
opam install ocamlfind
( 時点, 1.8.1は最新です)conf-m4
に依存します
opam install num
( 時点, 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
( 時点, 最新版)conf-findutils
に依存します- 必要なら, 最新のCoqIDEも設定できます:
opam install coqide
(10つ以上の依存するライブラリも設定されます) - Debian/Ubuntuで 新しいライブラリの設定が要るかもしれません:
libgtksourceview-3.0-dev
,libgtk-3-dev
,libexpat1-dev
,libcairo2-dev
(など?) (pkg-config
は要らなくなりましたか?)
- Coqのリポジトリを追加:
- 最後に, 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に関する追加情報:
- Coqのサイトによる設定方法
- MathCompによる設定の説明
opam pin
を用いる
2.1.2 ソースコードからのコンパイル
コンパイルのために必要なソフトウェアは通常のシステムで既にあるオープンソースソフトウェアです. Unix系なら, パッケージマネージャーから得られます. 必要なソフトウェアの情報のまとめ:
- GNU make (バージョン >= 3.81)
- C compiler
- TeX/LaTeX (ドキュメントのため)
- OCaml (バージョン >= 4.05.0;
ocaml -version
) ( 時点の最新版: 4.12.0) (インストール) - ZArith ( 時点、最新版: 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
, 最新版 : 8.00, transitionalモード?)- 不要になりましたか?
- ソースコードのアーカイブからコンパイル
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
- または, アーカイブを ダウンロード します
- gitで:
- できたディレクトリを
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
のコンパイル成功報告:- 既存のMathCompを削除したほうが無難です
COQINSTALLDIRECTORY/user-contrib
のmathcomp
ディレクトリを削除か名前変更します
- 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・方法2: cygwinの設定
- cygwinをインストールするよう, https://www.cygwin.com/から,
setup-x86_64.exe
(最新版: 2.897 )をダウンロードして, 実行します.- 最低限として,
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の実行ができます
- そうすると, System Trayアイコンの中に, Cygwin-X11アイコンができるます.
- 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
- cygwinをインストールするよう, https://www.cygwin.com/から,
- 方法3: WSLの設定
- Windowsのバージョンを確認します:
Windows Key + R
を入力し,winver
を実行します (ref).- 必要であれば1903以降のバージョンにアップデートします
- WSL本体と好きなLinuxディストリビューションをインストールします (ref):
- 管理者としてWindows PowerShellを起動
Enable-WindowsOptionalFeature -Online -FeatureName Microsoft-Windows-Subsystem-Linux
を実行します- 再起動します
- Microsoft Storeから, Linuxのディストリビューションをダウンロード・設定します
- Debian GNU/Linuxは広く使われています. Linux初心者の方にはUbuntu 18.04をおすすめします
- スタートメニューまたはWindowsの検索窓からLinuxを起動します
- ユーザー名とパスワードを入力します
- パッケージマネージャーを使って, 基本的なソフトウェアをインストールします:
- Ubuntu 18.04の場合には
sudo add-apt-repository ppa:avsm/ppa
を実行します sudo apt update
sudo apt-get install emacs
- Ubuntu 18.04の場合には
- WSL上でemacsを使いたいなら, Xorgサーバーは便利でしょう
- VcXsrvをダウンロードして, インストールします
XLaunch
アイコンでVcXsrvを起動しますmultiple windows
・start no client
を選びます
- WSLのshellで
DISPLAY
という環境変数の設定も必要です:export DISPLAY=localhost:0.0
.bashrc
にそのコマンドを追加できます (Ubuntu 18.04で確認済み)- VcXsrvを起動して, bashを再起動するとX上emacsが使えます
- Windowsのバージョンを確認します:
2.2.2 方法1 (cygwin + バイナリ)
- 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/
を追加します.
- 例えば,
- releaseページから
- 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のライブラリなどが追加されます.
- Coqのバイナリでは配布されているMathCompは最新ではないかもしれません.
2.2.3 方法2 (cygwin + opam)
過去にcygwinのOCamlパッケージの問題はよくあった(ライブラリは足りないこと; flexdll
のありなし)し,
cygwinで配るopamで設定するOCamlを用いてCoqのコンパイルができなかったので,
その2つの方法を使っていません. 代わりに, 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
( 's version: 7.06)opam install ocamlfind
( 's version: 1.8.0)conf-m4
も設定されますopam install depext
opam install depext-cygwinports
( '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
- cygwinで次のパケージを設定します:
- 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をインストールします:
sudo apt install opam
opam init --disable-sandboxing
(近い将来--disable-sandboxing
は要らなくなるそうです)- 時間がかかります.
opam switch create 4.08.1
- 時間がかかります.
- Debianに基づくディストリビューション以外の場合にはopamのウェブサイトを参照.
opam install coq
- 現時点最 新版8.9.1
- 時間がかかります.
- 開発版の設定には (
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 過去の設定報告メモ(参考のため)
flexdll
0.35を含みます. mingw64のパッケージがmingw64-x86_64-xxx
となりました.
にcygwin64が - Coq 8.5beta2で成功しましたが, math-compのMakefileが正しくファイルの依存関係を理解しません( の時点).
- Windows 8.1 + cygwin64上でcoq-8.5beta1, ssreflect-1.5.coq85beta1/mathcomp-1.5.coq85beta1Coq 8.5beta1のコンパイル成功しました.
- 主な問題: 現在
- flexdll のソースコードをダウンロードします(現時点の最新版:0.34).
一時的にcygwin64のOCamlパッケージを設定し,
mingw64_x86_64-{binutils,gcc-core,runtime}~等も設定します. flexlink.exe等を得るために, ~make demo_mingw64
を行います. 成功したら, cygwin64のOCamlパッケージを外し,PATH
に作業ディレクトリを追加します. - cygwin64のOCamlパッケージを外して, ソースからコンパイルします.
のcygwin64のOCamlは動的リンクライブラリをサポートしないため, flexdllからの再コンパイルが必要です.
- flexdll のソースコードをダウンロードします(現時点の最新版:0.34).
一時的にcygwin64のOCamlパッケージを設定し,
- その他の問題:
- Camlp5の設定:
./configure; make world; make install
は成功しますが, なぜかgramlib.a
を手動で/cygdrive/c/ocamlmgw64/lib/camlp5
までコピーしなければなりません. - MathComp-1.5の設定:
mathcomp-1.5.coq85beta1.tar.gz
でmake
が成功しますが, Error: Could not compile the library to native codeが発生します.make install
は完成します.
- Camlp5の設定:
- 過去に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の設定成功報告
- 設定済みの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の正しい設定を確 認します.
:
- [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などの設定ができます.
- [ALTERNATIVE] ソースコードのアーカイブ・githubからのCoqをのコンパイル
OCamlやcamlp5等を設定してたら, CoqのソースコードのアーカイブとgithubのMathCompの設定もできます. Windows 10で
configure
によると( ):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
( 時点,https://coq.inria.fr/download
から見つからなってきました) を ダウンロード・インストールし, そして 原将己のページからssreflect-windows-1.5-8.4pl5
とmathcomp-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 追加情報
ソースコードやバイナリのダウンロードのまとめ: