Coq/SSReflect/MathCompの設定

Table of Contents

1 更新

  • [2018-04-25 Wed]: Debian 9.4でopamによるOCaml 4.04.2とCoq 8.8.0のソースコードから・MathCompのgithubからの設定成功.
  • [2018-03-08 Thu]: Windows 10でopamによるOCaml 4.04.0/Debian 9.3でopamによるOCaml 4.04.2とCoq 8.7.2のソースコードから・MathCompのgithubからの設定成功.
  • [2018-01-16 Tue]: Windows 10でopamによるOCaml 4.04.0とCoq 8.7.1のソースコードから・MathCompのgithubからの設定成功.
  • [2017-11-28 Tue]: Windows 10でopamによるOCamlとCoq 8.7.0のソースコードから・MathCompのgithubからの設定成功.
  • [2017-10-24 Tue]: Debian 9.1でCoq 8.7.0のソースコードからとMathCompのgithubから, opamによるCoq 8.7.0とMathComp 1.6.2の設定成功.
  • [2017-09-29 Fri]: Debian 9.1でCoq 8.7-beta1のソースコードからとMathCompのgithubから, opamによるCoq 8.6.1とMathComp 1.6.1の設定成功.
  • [2017-07-26 Wed]: Debian 9.1でCoq 8.6.1のソースコードからとMathCompのgithubからの設定成功.
  • [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では, ソースコードからコンパイルすることは手間がかかります.

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

2.1.1 パッケージからの設定

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

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

MathCompによる設定の説明

  • 最初に, opamを設定します:
    • wget https://raw.github.com/ocaml/opam/master/shell/opam_installer.sh -O - | sh -s /usr/local/bin/
      • -O はminus zeroではありません
      • superuserになる必要があります
      • makegcc が要ります
    • opam init (y を選択します)
      • コンパイラを指定できます: opam init --comp=4.04.2 (例)
    • opamは既に設定された場合, 最新のパッケージの情報を取得: opam update
    • 使えるパッケージのリスト: opam list -a
  • 次に, OCamlの環境を設定します:
    • opam switch 4.05.0
      • opam switch list からその他のOCamlのコンパイラを選べます. 現時点[2017-09-29 Fri], 4.05.0は最新です.
    • eval `opam config env`
      • opam switch を行った後, 必要です.
    • 次のOCamlのプログラムはCoqに必要です(自分の環境の整備によって, 他のプログラムを設定する必要があるかもしれませんが, opamが教えます):
      • opam install camlp5 (現時点[2017-09-29 Fri], 7.01は最新です)
      • opam install ocamlfind (現時点[2017-09-29 Fri], 1.7.3は最新です)
  • 次に, Coqを設定します:
    • Coqのリポジトリを追加: opam repo add coq-released https://coq.inria.fr/opam/released
    • opam install coq.8.8.0
      • 必要なら, 最新のCoqIDEも設定できます: opam install coqide.8.8.0 (Debianで libgtksourceview2.0-dev の設定が必要です)
  • 最後に, MathCompを設定します:
    • opam install coq-mathcomp-ssreflect.1.7.0
    • その他のMathCompのパッケージ(prefixは coq-mathcomp です, バージョン1.7.0):
      • coq-mathcomp-algebra
      • coq-mathcomp-character
      • coq-mathcomp-field
      • coq-mathcomp-fingroup
      • coq-mathcomp-solvable
      • coq-mathcomp-sum-of-two-square, coq-mathcomp-multinomials (user contrib)
      • coq-mathcomp-odd-order (先端な応用ですので, 要らないかもしれません)
  • 今度の更新は, opam update , opam upgrade coq.8.8.0 (例えば) で済みます. 要らなくなったパッケージは opam remove coq-mathcomp-odd-order (例えば)で消せます.

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

コンパイルのために必要なソフトウェアは通常のシステムで既にあるオープンソースソフトウェアです. Unix系なら, パッケージマネージャーから得られます. 必要なソフトウェアの情報のまとめ:

  • GNU make (バージョン >= 3.81)
  • C compiler
  • TeX/LaTeX (ドキュメントのため)
  • OCaml (バージョン >= 4.01.0; ocaml -version) (最新版[2017-07-26 Wed]: 4.04.2) (ダウンロード)
  • Camlp5 (バージョン >= 6.02; camlp5 -v, 最新版[2018-01-16 Tue]: 7.03, transitionalモード)
  1. ソースコードのアーカイブからコンパイル

    Coq 8.8.0[2018-04-25 Wed](SSReflectの一部を含みます)のコンパイル成功報告:

    • ocamlc などを使える状態かを確認します(Unixで $PATH に入っていますか? 例えば, ocamlc -v を試します)
    • COQCOMPILEDIRECTORY というディレクトリでコンパイル作業します
    • Coqをダウンロード します
    • Coqをソースコードからコンパイルします
      • tar xzf coq-8.8.0.tar.gz (coq-8.8.0 というディレクトリは作成されます)
      • cd coq-8.8.0
      • ./configure
        • -usecamlp5 オプションは要らなくなりました
        • バイナリの位置に関して, デフォルト選択で結構です (バイナリは /usr/local/bin, ライブラリは /usr/local/lib/coq 等)
        • バイナリのインストールは不要なら, -local を使います
        • バイナリのインストールの場所を指定するために, -prefix を使います
        • lablGtk2を指すために, -lablgtkdir /DIR を使えるそうです
        • LablGtk2を見つからないと, CoqIdeをコンパイルできませんが, Coqをちゃんとコンパイルできます
      • make (ちょっと時間がかかりますので, -j で並列コンパイルしてみます)
        • make byte でバイトコード版ができます
      • sudo make install
        • superuserにならないと, デフォルト選択(/usr/local/bin 等)でのインストールが失敗します
        • -local なら不要, superuserにならなくいいです
        • SSReflectのプラッグインとセオリーの一部は COQINSTALLDIRECTORY/coq-8.7.2/plugins/{ssr,ssrmatching}/ に置かれます.
      • make clean (-local の場合以外)
      • cd ..
    • coqtop等は使えるようになった状態であるかどうかを確認します
      • 特に, Unixで $PATH に追加します
      • export COQBIN=COQINSTALLDIRECTORY/coq-8.8.0/bin/ という変数を作っておいていいです
    • テスト:
    $ coqtop
    Welcome to Coq 8.8.0 (April 2018)
    
    Coq < 
    

    [NB: 更新要] MathComp 1.6.1[2016-12-21 Wed]のコンパイル成功報告:

    • 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 MCINSTALLDIRECTORY/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. githubからのコンパイル

    [NB: 更新要] Coq 8.6をコンパイルします.

    • 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([2018-04-25 Wed]版)をコンパイルします(SSReflectの一部を含みます):

    • githubからソースコードを取得します: git clone https://github.com/math-comp/math-comp.git
    • cd math-comp/mathcomp
    • 開発版のCoqを見つかるように: export COQBIN=COQINSTALLDIRECTORY/coq-8.8.0/bin/
    • make
      • ちょっと時間がかかります
    • sudo make install
      • COQINSTALLDIRECTORY/coq-8.8.0/user-contrib/mathcomp でバイナリは置かれます.
        • 個人アカウントでバイナリを置くようにした場合, sudo は不要です.
      • SSReflectの一部は COQINSTALLDIRECTORY/coq-8.8.0/plugins/{ssr,ssrmatching}/ にすでにあります.
    • バイナリは通常の場所に置かれていない場合, coqc あるいは coqtop に教える必要があります. ただし, 指定がない場合, COQINSTALLDIRECTORY/coq-8.8.0/user-contrib を見に行きますので, 特別な設定はないかぎりに, -R のオプションは不要になります. それ以外, プラッグインとバイナリが見つかるように, -R COQINSTALLDIRECTORY/coq-8.8.0/user-contrib/mathcomp mathcomp オプションを追加できます.
    $ coqtop 
    Welcome to Coq 8.8.0 (April 2018)
    
    Coq < From mathcomp Require Import eqtype.
    [Loading ML file ssrmatching_plugin.cmxs ... done]
    [Loading ML file ssreflect_plugin.cmxs ... done]
    
    Coq < 
    

2.2 Windowsの場合

2.2.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.2.2 ソースコードからのコンパイル

Windowsだと, CygwinでUnixの場合のようなコンパイル方法は基本的に成功しますが, WindowsでのCoqの設定は長い歴史の問題があります.

ソースコードのアーカイブからコンパイルに必要なソフトウェアはcygwinから得られます. 必要なソフトウェアはUnixの場合とほとんど一緒です. 今までflexdllも要りました.

  1. 準備1: cygwin

    ソースから設定すると, Unix系のshellのインターフェスが便利ですので, cygwinの設定を勧めます.

    • cywinをインストールするよう, https://www.cygwin.com/から, setup-x86_64.exe (最新版: 2.9.0 [2017-11-28 Tue])をダウンロードして, 実行します.
    • 最低限として, emacs, xinit, make, texlive のパケージを選びます.
    • .bashrcexport LANG=C が望ましいです.
    • startxwin でX11を起動します. Windowsのタスクバーで見つかるcygwinのアイコンから, 「システムツール」のメニューから xterm 等を起動ができます.
    • cygwinに関するその他の情報(例えば, cygwinのアンインストール): cygwin faq
  2. 準備2: OCaml

    1. opamによるOCaml等の設定

      Windowsでもopamを使えるようになりました([2017-11-28 Tue]). このページの手動の手順をまとめます(graphicalインストーラはまだ確認していません):

      • cygwinで次のパケージを設定します:
        • rsync
        • patch
        • diffutils
        • curl
        • make
        • unzip
        • git
        • m4
        • perl
        • mingw64-x8664-gcc-core (or mingw64-i686-gcc-core)
      • opamをダウンロードします.
      • shellで次のコマンドを実行します:
        • tar -xf opam64.tar.xz
        • bash opam64/install.sh
        • opam init mingw 'https://github.com/fdopen/opam-repository-mingw.git' --comp 4.02.3+mingw64c --switch 4.02.3+mingw64c
          • .bash_profile.ocamlinit を変更していい
          • その後, opam switch 4.03.0+mingw64c, opam switch 4.04.0+mingw64c ができる
          • ただし, permission denied問題が発生することがあります. 原因不明. ディレクトリーのpermissionを緩めて, 管理者としてcygwinを実行して, 実行を繰り返すと成功するもあります. 下記の設定も同じ問題があります.
      • eval $(opam config env)
      • opam install camlp5 ([2018-01-16 Tue]'s version: 7.03)
      • opam install ocamlfind ([2018-01-16 Tue]'s version: 1.7.3-1)
        • conf-m4 も設定されます
      • lablgtkのため
        • opam install depext
          • 成功したことがある
        • opam install depext-cygwinports ([2018-01-16 Tue]'s version: 0.0.6)
          • 成功したことがある
          • その後, /usr/x86_64-w64-mingw32/sys-root/mingw/bin をパスに加える.
        • opam install pcre
          • 成功したことがある
        • opam install lablgtk
          • 成功したことはない

      以上, OCaml等の設定ができますが, opamを用いてCoqの設定は成功したことないです:

      • [X] opam repo add coq-released https://coq.inria.fr/opam/released
      • [ ] opam install coq.8.7.{0,1}
        • num, base, ~base-num~しか設定できたことはない
    2. ソースからの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 に追加します.
    3. cygwinのOCamlについて

      過去にcygwinのOCamlパッケージの問題はよくありました(ライブラリは足りないこと; flexdll のありなし)ので, 最近使っていません.

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

    opamでOCamlやcamlp5等を設定してたら, CoqのソースコードのアーカイブとgithubのMathCompの設定が成功しました. Unixの場合と同じ手順ですが, cygwinのせいでコンパイルは遅くなります. 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
    

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

    • [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=). 等の問題.

2.3 MacOSの場合

opam?

2.4 その他の設定方法

  • Linuxの仮想機械(例えば, VirtualBox)で作業することは時々聞きますが, 仮想機械のfreezeは目撃したことがあります. Coqのwiki で詳細な情報があります.
  • MathLibreのDVDにCoqとSSReflectとMathCompが入っています.
  • 他のSSReflect/MathCompのバイナリ:
  • 原将己によるのバイナリ(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モードをお勧めします. Coqを設定すると, CoqIDEという専用インターフェースも設定されます.

Proof Generalはemacsエディターのモードです. Unixなら, emacsは必ず入っています. Windowsなら, cygwinで取得できます. Proof Generalはgitを経て設定します(旧サイト: http://proofgeneral.inf.ed.ac.uk/) (最新版[2017-10-24 Tue]: 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のバイナリは 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: 2018-05-18 Fri 11:07

Validate