ProofGeneral と ssreflect のインストール

はじめに

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.

以上