ProofGeneral と ssreflect のインストール

1688 ワード
Coq Coq テキストリンク

はじめに

coqide + ssreflect のインストール方法は調べても分からなかったので、ProofGeneral を選択。
ssreflect は opam でもインンストールできて ProofGeneral との連携もできると思うが、そもそも ProofGeneral との連携方法が分かっていない時にインストールしたので、実際にはチャレンジしていない。

インストール成功手順

  • homebrewでcoqをイントール

  • math-comp-mathcomp-1.7.0のソースを落として来て、INSTALL.md 通りにインストール

    展開して、coqcのパスがあることを確認して、mathcompに移動。make
  • ProofGeneral を Quick installation とおりにインストール
    git clone https://github.com/ProofGeneral/PG ~/.emacs.d/lisp/PG
    cd ~/.emacs.d/lisp/PG
    make
  • .emacsに以下を記入
    ;; Open .v files with Proof General's Coq mode
    (load-file "~/.emacs.d/lisp/PG/generic/proof-site.el")
    (load-file "/Users/hogehoge/math-comp-mathcomp-1.7.0/mathcomp/ssreflect/pg-ssr.el")
    (setq coq-prog-name "/usr/local/bin/coqtop")
  • ソースコード(0529.v)と同一ディレクトリに _CoqProject ファイルを作成し中身に以下を記入
    -R "/Users/hogehoge/math-comp-mathcomp-1.7.0/mathcom" mathcomp
  • ソースコード上に From mathcomp の記述があるとだめなようなので、以下のみ記述
    Require Import ssreflect.

以上