Coqシステムの使い方

  1. 最初に1回だけやること

    Coqシステムを使うために，本演習では， emacs 上の Proof General というライブラリを使う． よって、Proof General と Coq に関する設定が必要である．

    設定1. 以下の記述(~kam/coq/dot-emacs)を，自分の home directory のすぐ下にある .emacsファイル(ドットemacsファイル) の一番下に追加しなさい． 

    (load "/opt/local/share/ProofGeneral/generic/proof-site.el")
(defadvice coq-mode-config (after deactivate-holes-mode () activate)
  "Deactivate holes-mode when coq-mode is activated."
  (progn (holes-mode 0))
)
(add-hook 'proof-mode-hook
   '(lambda ()
      (define-key proof-mode-map (kbd "C-c C-j") 'proof-goto-point)))

    なお，これを打ち込むのは大変なので，以下のようにするとよい． 

    cat ~kam/coq/dot-emacs ~/.emacs > ~/temp
mv ~/temp ~/.emacs

    設定2. Coq の実行ファイルの場所が，自分の(MacOS における)実行可能 ファイルを置く path にはいっていることを確認し，はいっていなければ 追加する．たとえば，(Macの「端末」ウィンドウにおいて) 

    coqc -v
    とやってみて，Coq のバージョンが表示されれば成功である． 表示されないときは，自分のシェルの設定ファイル (~/.bashrc など)をチェッ クして，/opt/local/bin/ が path にはいっているか確認せよ．

  2. 最初に1回と，その後時々やること

    本講義のファイルを自分のホームディレクトリの下の適当な 場所にコピーしよう．ここでは ~/complogic という名前とする。 本講義のファイルは、~kam/coq/ にある． よって，以下のようにしてほしい． 

       mkdir ~/complogic
   cp ~kam/coq/* ~/complogic
    これで，xxx.v および yyy.vo というファイルがいくつか コピーできたはずである． (最初は PropLogic.v, PropLogicDef.v, PropLogicDef.vo, SfLib.v, SfLib.vo がコピーされる．)

    これらは1回だけコピーすればよいが， 来週以降の演習では，新しい xxx.v というファイルを使ったり， PropLogicDef.v をバージョンアップすることがあり得るので， (そのような場合は，連絡する．) その際には cp ~kam/coq/yyy.v ~/complogic として コピーする必要がある．

  3. 毎回やること

    上記設定がしてあれば， emacsを起動したあと，xxx.v というファイルを読みこめば， 自動的にCoq Proof Generalモードになる． たとえば，emacs から PropLogic.v というファイルを読み込めば良い．

  4. Coq Proof General (Proof General 上で使うCoq) の使い方

    メニューバーにいろいろなメニューがあるが， カーソルの動かしかたとしては， 当面，以下のものだけで十分であろう．

    なお、C-c 等は、controlキーを押しながら、c をタイプするという意味である。

  5. Coq Proof Generalの終了方法

    PropLogic.v など，Coqの証明がはいっているファイルの編集を終了する ときは，そのファイルのバッファを kill すればよい．(PropLogic.v と いう名前のバッファにいって，C-c k とするとよい．もし，そのファイルを セーブしていないときは，セーブするかを聞かれるので yes/no を答える．) 最終的に emacs を終了すれば，Proof General も Coq も自動的に終了する． (emacs からは，C-x C-c で抜けられる．)

  6. 自分のノートPC 等での利用について

    演習を自分のノートPC 等で行なうことは，まったく問題ない． 自分で Coq (version 8.4) と最新の Proof General をインストールして， Proplogic.v などのファイルをコピーしてくればよい． 自力での Coq等のインストールについては，特にサポートしないが， Linux系や Mac のOSを使っていれば aptitude/port 等のパッケージ管理ソフトで coq と proofgeneral をインストールするだけで済む．

  7. CoqIDE について

    Coq を使うためには，Proof General のほか，CoqIDEというウィンドウベース のシステムを使ってもよい．こちらは，emacs 上ではなく，単純にウィンドウ 上で動くので，自分のノートPC等でやってみるのもよいだろう． (coinsマシン上には，CoqIDEはインストールされていないようである．)

Yukiyoshi Kameyama