Coq/SSReflect/MathCompの設定

Table of Contents

1 更新

  • [2017-01-12 Thu]: Windows 8.1でopamによるCoqの設定成功報告.
  • [2017-01-06 Fri]: Debian 8.6でopamによる設定成功報告.
  • [2016-12-21 Wed]: Debian 8.6とUbuntu 16.04.1 LTSで, opamによるOCaml 4.04.0を用いて, Coq 8.6とMathComp 1.6.1をソースコードからの設定成功報告と CoqとMathCompのgithubのソースコードからの設定成功報告.
  • [2016-02-01 Mon]: Coq 8.5/MathComp 1.6をWindows 8.1でバイナリを用いて設定成功報告とLinux(Ubuntu Server 14.04.1 LTS)でソースコードからのコンパイル成功報告.
  • [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-12-11 Thu]: 第三者によるWindowsでバイナリからの設定成功報告とMathLibreへのリンクの追加.
  • [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系のオペレーティングシステムでスムーズです. opamによる設定は簡単ですが, 最新のパッケージが出来上がるまでに時間がかかります. Unix系のオペレーティングシステムでソースコードからコンパイルすることもスムーズですので, 最新版を設定する方法として勧めます. Windowsの場合, バイナリが用意されています. 一方, Windowsでは, ソースコードからコンパイルすることは手間がかかります.

インターフェースとして, emacsに慣れているのでしたら, Proof General というemacsモードをお勧めします. Coqを設定すると, CoqIDEという専用インターフェースも設定されます.

2.1 パッケージやバイナリからの設定

2.1.1 Unix系のオペレーティングシステムの場合

Linuxのパッケージマネージャー(Debianのapt等)のCoqのバージョンはいつも遅れていますので, 勧められません.

Ocamlの専用パッケージマネージャーopam でCoqのパッケージを設定ができます. Debianのaptほど遅れていません. opamで, SSReflectとMathCompを含むCoqライブラリが用意されています(Coq OPAM packages). 現時点[2017-01-06 Fri], opam show coq-mathcomp-ssreflect によると, 1.6.1版のパッケージがあります.

  • 最初に, opamを設定します:
    • wget https://raw.github.com/ocaml/opam/master/shell/opam_installer.sh -O - | sh -s /usr/local/bin/ (-O はminus zeroではありません. superuserになる必要があります.)
    • opam init (y を選択します.)
  • opamは既に設定された場合, 最新のパッケージに更新: opam updateopam upgrade
  • 次に, Ocamlの環境を設定します:
    • opam switch 4.04.0 (opam switch list からその他のOCamlのコンパイラを選べます. 現時点[2017-01-06 Fri], 4.04.0は最新です.)
    • 次のOCamlのプログラムはCoqに必要です(自分の環境の整備によって, 他のプログラムを設定する必要があるかもしれませんが, opamが教えます):
      • opam install camlp5 (現時点[2017-01-06 Fri], 6.17は最新です)
      • opam install ocamlfind (現時点[2017-01-06 Fri], 1.7.1は最新です)
    • eval `opam config env` (opam switch を行った後, 必要です.)
  • 最後に, Coqなどを設定します:
    • Coqのリポジトリを追加します: opam repo add coq-released https://coq.inria.fr/opam/released
    • 使えるパッケージのリスト: opam list -a
    • 必要なら, Coqを設定します: opam install coq.8.6
      • 必要なら, 最新のCoqIDEを設定します: opam install coqide.8.6 (Debianで libgtksourceview2.0-dev の設定が必要です)
    • SSReflectを設定します: opam install coq-mathcomp-ssreflect.1.6.1
      • その他のMathCompのパッケージ: coq-mathcomp-algebra, coq-mathcomp-character, coq-mathcomp-field, coq-mathcomp-fingroup, coq-mathcomp-solvable, coq-mathcomp-sum-of-two-square

2.1.2 Windowsの場合

  1. Windowsインストーラ

    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の正しい設定を確認します.
  2. opam

    [2017-01-12 Thu]時点, Windowsでもopamを使えるようになりましたが, まだ不安定みたいです.

    • [2015-09-07 Mon]時点: cygwin64でのソースからのコンパイルは失敗しました; cygwin64との相性は悪いみたいです; cygwin32なら, opamはあるそうですが、自分で動作確認しませんでした.

    opamのインストール をそのまま成功します (現時点[2017-01-12 Thu]の最新版は[2016-07-18 Mon]). (手動で, cywginを用いて, opam install depext depext-cygwinports まで確認しました. graphicalインストーラはまだ確認していません.) ただし, opamを設定してから, 上記のopamによるMathCompの設定は完全に通りません:

    • [X] opam install camlp5
    • [X] opam install ocamlfind
    • [X] eval `opam config env`
    • [X] opam repo add coq-released https://coq.inria.fr/opam/released
    • [X] opam install coq.8.6
    • [ ] opam install coqide.8.6 (opam depext conf-pkg-config.1.0 を行っても, pkg-config, libgtksourceview2.0-devel のcygwinを設定しても, missing external dependencies で設定は失敗します.)
    • [ ] opam install coq-mathcomp-ssreflect.1.6.1 (Windowsのpathを読み間違い見たいです.)

    これから, MathCompのソースからのコンパイルはすぐ通らなかったです(検討中).

  3. その他
    • Linuxの仮想機械(例えば, VirtualBoxで作業することは時々聞きますが, 仮想機械のfreezeは目撃したことがあります.
    • MathLibreのDVDにCoqとSSReflectとMathCompが入っています.
    • 他のSSReflect/MathCompのバイナリ:
    • 原将己によるのバイナリ(Coq8.4pl5まで). 次の手順で設定できます. Coqのダウンロードページから coq-installer-8.4pl5.exe を ダウンロード・インストールし, そして 原将己のページから ssreflect-windows-1.5-8.4pl5mathcomp-windows-1.5-8.4pl5 をダウンロードし, 適切にコピーします.

2.2 Proof Generalの設定

Proof Generalはemacsエディターのモードです. emacsはUnixなら必ず入っています. Windowsなら, cygwinで取得できます. Proof Generalはgitを経て設定します(旧サイト: http://proofgeneral.inf.ed.ac.uk/) (最新版[2016-12-21 Wed]: 4.4.1~pre):

  • git clone https://github.com/ProofGeneral/PG ~/.emacs.d/lisp/PG
  • cd ~/.emacs.d/lisp/PG
  • make
  • 自分のホームディレクトリで, .emacs というファイルを編集します:
    • Proof Generalを使うために:
    ;; Open .v files with Proof General's Coq mode
    (load "~/.emacs.d/lisp/PG/generic/proof-site")
    
    • デフォルトな場所でSSReflectとMathCompのバイナリは置いていない場合は, Coqに教える必要があります. 例えば:
    (setq coq-prog-args
      (cons "-R" (cons "/MYINSTALLDIRECTORY/math-comp/mathcomp" (cons "mathcomp" (cons "-emacs" nil)))))
    
  • emacsでtt.vという空のファイルを開いてみて, Proof Generalが機動するかどうかを確認します.
    • From Ssreflect Require Import ssreflect. を通れば, 問題ないでしょう.

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

コンパイルのために必要なソフトウェア(makeなど)は通常のシステムで既にあるオープンソースソフトウェアです. Unix系なら, パッケージマネージャーから得られます. Windowsなら, cygwin からほとんど全ての必要なオープンソースソフトウェアを得られます.

必要なソフトウェアの情報のまとめ:

  • GNU make (バージョン >= 3.81)
  • C compiler
  • TeX/LaTeX (ドキュメントのため)
  • OCaml (バージョン >= 4.01.0; ocaml -version) (最新版[2016-12-21 Wed]: 4.04.0) (ダウンロード)
  • Camlp5 (バージョン >= 6.02; camlp5 -v, 最新版[2016-12-21 Wed]: 6.17, transitionalモード)
  • flexdll (cygwin64でのOCamlの再コンパイルのため)

2.3.1 Unix系のオペレーティングシステムでのコンパイル

  1. githubからのコンパイル

    Coq 8.6とSSReflect/MathComp 1.6.1のコンパイル成功報告.

    • Coqをコンパイルします.
      • githubからソースコードを取得します: git clone https://github.com/coq/coq.git
      • cd coq
      • git ls-remote --heads
      • trunkブランチからv8.6ブランチに移動: git checkout v8.6
      • 開発版なので, 設定ディレクトリのままにします: ./configure -local -usecamlp5
      • make world
    • MathCompをコンパイルします. (SSReflectを含みます.)
      • githubからソースコードを取得します: git clone https://github.com/math-comp/math-comp.git
      • cd math-comp/mathcomp
      • 開発版のCoqを見つかるように: export COQBIN=/MYINSTALLDIRECTORY/coq/bin/
      • make
    • バイナリは通常の場所に置かれていないので, coqc あるいは coqtop に教える必要があります (基本的に, -R MYINSTALLDIRECTORY/math-comp/mathcomp mathcomp オプションの追加となります).

  2. ソースコードのアーカイブからコンパイル

    Coq 8.6とSSReflect/MathComp 1.6.1[2016-12-21 Wed]のコンパイル成功報告:

    • ocamlc などを使える状態かを確認します(Unixで $PATH に入っていますか? 例えば, ocamlc -v を試します)
    • /MYCOMPILEDIRECTORY というディレクトリでコンパイル作業します
    • Coqをダウンロード します
    • Coqをソースコードからコンパイルします
      • tar xzf coq-8.6.tar.gz (coq-8.6というディレクトリは作成されます)
      • cd coq-8.6
      • ./configure -usecamlp5
        • バイナリの位置に関して, デフォルト選択で結構です (バイナリは /usr/local/bin, ライブラリは /usr/local/lib/coq 等)
        • バイナリのインストールは不要なら, -local を使います
        • バイナリのインストールの場所を指定するために, -prefix を使います
        • lablGtk2を指すために, -lablgtkdir /DIR を使えるそうです
        • LablGtk2を見つからないと, CoqIdeをコンパイルできませんが, Coqをちゃんとコンパイルできます
      • make world (ちょっと時間がかかりますので, -j で並列コンパイルしてみます)
      • sudo make install (superuserにならないと, デフォルト選択(/usr/local/bin 等)でのインストールが失敗します)
      • make clean
      • cd ..
    • coqtop等は使えるようになった状態であるかどうかを確認します (特に, Unixで $PATH に入っていますか?). 例えば:
    $ coqtop
    Welcome to Coq 8.6 (December 2016)
    
    Coq <
    
    • Mathematical Componentsのsources archiveをダウンロード
    • Mathematical Componentsをコンパイルします:
      • tar xzf math-comp-mathcomp-1.6.1.tar.gz
      • cd math-comp-mathcomp-1.6.1
      • export COQBIN=/usr/local/bin/ (coqtop等のバイナリがあるディレクトリ)
      • cd mathcomp
      • make (ちょっと時間がかかりますので, -jオプションで並列コンパイルしてみます)
      • sudo make install (その結果で, ライブラリは /usr/local/lib/coq/user-contrib/mathcomp に置かれます. 1.5版までは /usr/local/lib/coq/user-contrib/Ssreflect/usr/local/lib/coq/user-contrib/MathComp でした.)
      • cd ../..
    • coqtop等は使えるようになった状態であるかどうかを確認します. 例えば:
    $ coqtop -R /MYINSTALLDIRECTORY/math-comp/mathcomp/ mathcomp
    Welcome to Coq 8.6 (December 2016)
    
    Coq < From mathcomp Require Import ssreflect.
    [Loading ML file ssrmatching_plugin.cmxs ... done]
    
    Small Scale Reflection version 1.6 loaded.
    Copyright 2005-2016 Microsoft Corporation and INRIA.
    Distributed under the terms of the CeCILL-B license.
    
    [Loading ML file ssreflect_plugin.cmxs ... done]
    
    Coq <
    

2.3.2 Windowsでのコンパイル

cygwinの設定について:

  • cywinをインストールするよう, setup-x86_64.exe (最新版: 2.6.1([2017-01-12 Thu]))を実行します. せめて, GNU make, emacs-X11, xinit, git, vim, texlive が要ります.
  • .bashrcexport LANG=C が望ましいです.
  • startxwin でX11が起動します. Windowsのタスクバーから, xterm 等を起動ができます.
  • cygwin faq (cygwinのアンインストール等)

注意: Windowsだと, Cygwinで, 上記のようなコンパイル方法は成功します. 但し, WindowsでのCoqの設定は長い歴史の問題があります. 次のリストは参考になるかもしれません. Cygwinのバージョンによって問題が生じることがあります: Cygwin自体の問題(例: export LANG=C), CygwinのOCamlパッケージの問題 (Coqのコンパイルのため, ライブラリは足りないこと; flexdll のありなし). 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= 等).

  1. githubからのコンパイル

    Windows + Cygwin上でUnix上の設定方法は基本的に通りますが, 相変わらず不思議なことがあります. Coq 8.5beta2で成功しましたが, math-compのMakefileが正しくファイルの依存関係を理解しません([2015-10-28 Wed]の時点).

  2. ソースコードのアーカイブからコンパイル

    NB: [2017-01-12 Thu] にcygwin64が flexdll 0.35を含みます. mingw64のパッケージが mingw64-x86_64-xxx となりました. ただし, 下記のコンパイル方法は再現できませんでした(検討中).

    Windows 8.1 + cygwin64上でOCaml 4.02.1, coq-8.5beta1, ssreflect-1.5.coq85beta1/mathcomp-1.5.coq85beta1Coq 8.5beta1のコンパイル成功報告 (上記の「Unix系のオペレーティングシステムでの設定」も参考になります). 主な問題: 現在[2015-04-04 Sat]のcygwin64のOCamlは動的リンクライブラリをサポートしないため, flexdllからの再コンパイルが必要です.

    • flexdllの設定:flexdll のソースコードをダウンロードします(最新版:0.34). 一時的にcygwin64のOCamlパッケージを設定し, mingw64x8664-{binutils,gcc-core,runtime}等も設定します. flexlink.exe等を得るために, make demo_mingw64 を行います. 成功したら, cygwin64のOCamlパッケージを外し, PATH に作業ディレクトリを追加します.
    • 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 に追加します.

    • Camlp5の設定: ./configure; make world; make install は成功しますが, なぜか gramlib.a を手動で /cygdrive/c/ocamlmgw64/lib/camlp5 までコピーしなければなりません.
    • Coq-8.5beta1の設定: ./configure -local でコンパイルします.
    • SSReflect-1.5の設定: ssreflect-1.5.coq85beta1.tar.gz を取得します. COQBIN 変数を coqtop 等のディレクトリに設定し, PATH に追加します make; make install は成功します.
    • MathComp-1.5の設定: mathcomp-1.5.coq85beta1.tar.gz を取得します. make が成功しますが, Error: Could not compile the library to native codeが発生します. make install が完成します.

2.4 追加情報

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

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

Author: Reynald Affeldt

Created: 2017-01-27 Fri 18:41

Emacs 24.4.1 (Org mode 8.2.10)

Validate