Coq 8.6のインストールほか

Coq 8.6をインストールしたときのあれこれ

Coqのインストール

Coq/SSReflect/MathCompの設定

これの通りにやるだけ
aptのパッケージは古いからだめってあったので言われたとおりにopamでいれた

それと~/.opam/4.04.0/binにパスを通すのもやった.
どうもopamはバージョンごとにbinディレクトリを分けてるみたいなのでバージョン上げるときは注意(面倒だからやめてほしい).

ssreflectを入れた場合は

From mathcomp Require Import ssreflect.

が通るかを確認.

ProofGenral

基本は上の通り.

Input methodをAgdaにした(unicode symbolsをカジュアルに使うため, TeXでもいいけど最高に使いづらかったのでAgdaにした).
当然のことながらagda-modeが入ってるのが前提

;; proof general
(when (file-directory-p "~/.emacs.d/lisp/PG")
  (load "~/.emacs.d/lisp/PG/generic/proof-site")

  (require 'agda-input)
  (add-hook 'proof-mode-hook (lambda () (set-input-method "Agda"))))

以上.
とっても簡単.