自分のCoq環境 (with Vim)

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

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

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

自分のCoq環境

基本情報

  • MacOS
  • NeoVim v0.3.7
  • Coq v8.10.1

coquille

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

github.com

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

1: Infosパネルが空

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

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

github.com

2: highlightが効かない

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

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

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

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

(2019/11/11 追記) Coq v8.9.0以降の対応

Coqv8.9.0以降では、 coqtop -ideslave の代わりとして coqidetop を使うようになったようなので、その部分を修正して動くようにしました。

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

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

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

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

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

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