Emacs & ProofGeneral で Coq 使い分け

  • 10
    いいね
  • 0
    コメント
この記事は最終更新日から1年以上が経過しています。

Emacs & ProofGeneral で Coq 使い分け

9/7 (sun) にコードを更新しました.
環境変数も良い感じに処理するようにしたので, eshell 上でも切り替えが作用します.


Emacs で ProofGeneral ユーザな複数の Coq バイナリを使い分けたい方々を対象としております.
コードは下部にありますので,コードが目当ての方は以降の文章は読まずに飛ばしちゃいましょう.

前書

Coq は現在 ver. 8.4pl4 ですが 8 月正式リリース予定の 8.5 で universe polymorphism が追加 されますね.
matthew さんの web ページから辿れる github リポジトリ から引っ張ってくれば,今からでも universe polymorphism と戯れることが出来ます.
What's universe polymorphism ? という方は このペーパーこのスライド を 読んでみると良いかもしれません.

本題

さて,なんやかんやと universe polymorphism と戯れていますが,一つ問題があるとすれば SSReflect が使えないことです.
昨今の Coq 事情を鑑みれば Coq とは即ち Coq + SSReflect であるわけですから,これは由々しき事態です.
しかし,対応していないものは仕方ない.
であれば,その時々に応じて

  • SSReflect の使える Coq
  • Universe Polymorphism の使える Coq

それぞれ使うバージョンを切り変えれば良いわけであります.

Universe Polymorphism と SSReflect の二択に悩んだり,複数バージョンの Coq を走らせたりする方々は数多くおられることと思います.
最近やっと Emacs Lisp を読み書きする気になりましたので,これもいい機会だと小さなコマンドを定義しましたので,ここに公開しておきます.
コピペしてパスを適当に書き換えて .emacs.el なり init.el なりに突っ込めばさくっと利用可能です.

もっと簡単に書けるでしょ! などご意見ございましたら twitter へお投げください.

;; Coq-Binary-Switcher
(setq coq-prog-name "your/path/of/coqtop")

(defvar coq-with-univ-poly nil)
(defvar path-template (getenv "PATH"))

(defun set-coq-path (binpath)
  (setenv "COQBIN" binpath)
  (setenv "PATH" (concatenate 'string binpath ":" path-template))
  (setq coq-prog-name (concatenate 'string binpath "coqtop")))

(defun coq-switch-bin ()
  (interactive)
  (if coq-with-univ-poly
      (progn
    (setq coq-with-univ-poly nil)
    (set-coq-path "/your/path/of/coq/bin/"))
    (progn
      (setq coq-with-univ-poly t)
      (set-coq-path "/your/path/of/univ/poly/coq/bin/"))))

解説的なもの

例えば僕の場合, ProofGeneral 起動後は SSReflect 利用可能,つまり Coq8.4pl4 のバイナリを利用する設定になっています.
ふと証明したくなった時に使うのは SSReflect ですからね.

また,coq-switch-bin コマンドの効果が現れるのは C-c C-x などで証明プロセスを一度終了させてからです.
証明中にコマンドを叩いても,そのプロセスの間は変更前のバージョンを利用しますので,ご注意ください.

ちなみに proof-prog-name の値は Coq 利用時であればプロセス開始時に自動的に coq-prog-name の値に書き換えられますが,なんとなく念の為についでとしてこのタイミングで変更してあります.

後書

需要とかそういうのは知らない.
ただ,書きたくなってしまったんだ.