自分のCoq環境 (with Vim)

一年前くらいにCoqを触り始めて、Software FoundationやCPDTなどを読みながら細々とCoqの勉強を続けています。

Coqを使うための環境としては、CoqIDEやProofGeneralなどが有名ですが、 前者はUIが充実していなくて使いにくく、後者はEmacsなので普段Vimを使っている自分にとっては抵抗がありました。

そのため、しばらく前からVimのCoqプラグインを使っているのですが、CoqのVim関連のソフトウェアはあまり充実していなくて使えるようになるまでに苦労したため、 どうやって導入したかを書き留めておこうと思います。

自分のCoq環境

基本情報

  • MacOS
  • NeoVim v0.3.4
  • Coq v8.8.1

coquille

VimのCoqプラグインで最適なものとしてはcoquilleがありましたが、2017年末以降開発が完全に止まっていて、プルリクもマージされない状態になっています。そのため私は、本家のcoquilleにパッチをあてている人のものにさらにパッチを当てたものを使っています:

github.com

本家のcoquilleが私の環境ではそのままでは使えなかった原因として次の2つがあります。

本家coquilleの問題点1: Infosパネルが空

本家レポジトリのpathogen_bundleブランチのバージョンでは、右下のInfosパネルに何も表示されないという問題がありました。これは新しいCoqのバージョン*1ではcoqtopが返す結果のフォーマットが変わっていたためです。

本家レポジトリのPull requestを眺めていると、このようなバグに対してパッチをあてている人がいたため、その人のcoquilleを代わりに使ってみたところこの問題は解消されました:

github.com

本家coquilleの問題点2: highlightが効かない

しかし、まだ1つ問題が残っていました。Coqに読み込まれた部分に色がつかないのです。

本来coquilleでは、Coqに読み込まれた部分にこんな感じで色がつきます。*2 f:id:momohatt:20190427171142p:plain:w500

しかし、私の環境でlucas8/coquilleを使用した場合は次のように色がつきませんでした。 f:id:momohatt:20190427171157p:plain:w500

調べたところ、Vimのカラースキームによってcoquilleのhighlightが上書きされてしまっているようだったので、coquilleのハイライトグループがカラースキームの読み込み後に定義されるように変更するパッチをあてたところうまく動くようになりました🎉

lucas8/coquilleにこのパッチを加えたものが私のmomohatt/coquilleになります。

ただし、同じくcoquilleを使おうとした私の友人は、カラースキームを使っているにも関わらず、lucas8/coquilleが動いた*3ようなので人によるのかもしれません。

opamでCoqのバージョンを固定する

実は上の方法はCoq v8.9以降では動かないのですが、coquilleをv8.9に対応させるのが面倒くさいのと Coqをv8.9にアップデートする積極的理由があまりないため、v8.8のままにして使っています。

しかし、opamで何かのライブラリなどをインストールするとたまに自動でCoqをアップデートしてしまうことがあるので、opam pinを使って勝手にCoqがアップデートされないようにしています。

(参考) 他のCoqプラグイン

私の環境では動かせていないので紹介にとどめますが、最近Coqtailという新しいプラグインが開発され始めているようです: github.com

私の環境で使おうとするとCoqStart でハングしてしまうという感じで全く使えないので、うまく動かせた方がいたら教えてほしいです🙏

*1:おそらく8.5以降とかだった気がします

*2:Coqに読み込まれるのを待っている部分にもつきますが、写真を撮るのが難しかったため

*3:momohatt/coquilleでは no such highlight group name: SentToCoq のエラーが出てしまった