自分の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にパッチをあてている人のものにさらにパッチを当てたものを使っています:
本家のcoquilleが私の環境ではそのまま使えなかった原因として次の2つがあります。
1: Infosパネルが空
本家レポジトリのpathogen_bundle
ブランチのバージョンでは、右下のInfosパネルに何も表示されないという問題がありました。これは新しいCoqのバージョン*1ではcoqtop
が返す結果のフォーマットが変わっていたためです。
本家レポジトリのPull requestを眺めていると、このようなバグに対してパッチをあてている人がいたため、その人のcoquilleを代わりに使ってみたところこの問題は解消されました:
2: highlightが効かない
本来coquilleでは、Coqに読み込まれた部分にこんな感じで色がつきます。*2
しかし、私の環境でdwarfmaster/coquilleを使用した場合は次のように色がつきませんでした。
調べたところ、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
でハングしてしまうという感じで全く使えないので、うまく動かせた方がいたら教えてほしいです🙏