Coq/SSReflect/MathCompのインストール

Coq/SSReflect/MathCompの UNIX系OSへのインストール    2019年10月時点

  • OSのパッケージ機能などのなんらかの手段で、OCaml および opam をインストールする。以下では、opamは、ver.2.0以降を前提とする。

  • ~/.cshrc などに、以下を追加する。
            eval `opam config env`

  • opamを初期化する。OCaml Ver.4.07.1 が使われ、~/.opam/4.07.1/ 以下にインストールされる。
            $ opam init
            $ opam update
            $ opam switch create 4.07.1 4.07.1
            $ eval `opam config env`
    
            要すれば、source ~/.cshrc の実行し、そのshell上で emacs を再起動する。環境によってはログイン・ログアウトが必要かもしれない。
            emacs本体に教えてあげる必要がある。なのでemacs上のshellの再起動だけではだめ。 

  • opam でCoqとSSReflectなどをインストールする。
            $ opam install coq.8.9.1
            $ opam repo add coq-released "https://coq.inria.fr/opam/released"
            $ opam install coq-ext-lib
            $ opam install coq-mathcomp-ssreflect
            $ opam install coq-mathcomp-algebra
            $ opam install coq-mathcomp-character
            $ opam install coq-mathcomp-analysis

  • ProofGeneralをインストールする。
            $ git clone https://github.com/ProofGeneral/PG
            $ cd PG
            $ vi Makefile            (/usr/local/share//site-lisp に入ったので、/usr/local/share/emacs/site-lisp になるように修正した)
            $ make
            $ su
            # make install
            # cp pg-ssr.el /usr/local/share/emacs/site-lisp

            pg-ssr.el は、mathcomp のソースコードに含まれている。たとえば、以下にあるはず。
            ~/.opam/4.07.1/.opam-switch/sources/coq-mathcomp-ssreflect.1.9.0/mathcomp/ssreflect/pg-ssr.el

以上

Comments