EasyCryptとProofgeneralのインストール

EasyCryptという暗号系の形式検証支援系をインストールしようとしたところ、詰まったところがたくさんあったので備忘録。
2019/11/12追記 ここを読まずに公式のGithubリポジトリの手順を読みましょう。

EasyCryptインストールまで

公式Githubを参考にインストールする。手順をおおまかに書くと、

  1. opam入れる
  2. opamにEasyCryptのリポジトリを追加する
  3. opam install depextしてopam depext easycryptする
  4. opam install --deps-only easycryptしてopam install ec-proversする
    ここまでしか書いていない資料があるが、これだけだとメタパッケージまでしか入っていないので、
  5. opam install easycryptする
  6. why3 config --detectする

5をしないと次のproofgeneralのインストールで詰まる。
なお親切な人がdockerイメージを配布しているので、4まではこれをつかって省略できる。

Proofgeneralのインストール

Coq等でおなじみProofgeneralは、公式でEasyCryptに対応している。

  1. opam install proofgeneralする
  2. emacsのパッケージアーカイブにMELPAを追加する。ここ参照
  3. package-install でexec-path-from-shellとopamをインストールする
  4. init.elに次を書き込む
(when (memq window-system '(mac ns))
  (exec-path-from-shell-initialize))

(opam-init)

そのあと.emacsに次を書き込む

(load-file "$proof-general-home/generic/proof-site.el")

ただし $proof-general-home には opam config var prefixで出力されたパスを入れる。

emacsもopamもほぼ全く使ったことがなかったのでめちゃくちゃ大変だった