Vim で Coq 環境を整える

はじめに

昨日、スタート Ssreflect というイベントに参加して、Coq + ssreflect のハンズオン的なものをやりました。 Coq 環境といえば、Emacs の ProofGeneral が非常に有名です。 しかし、私は Emacs は終了の仕方すら分からないレベルの初心者なので Emacs + ProofGeneral ではチュートリアルの例題を打ち込むだけでも非常に苦労しました。

証明も普段使い慣れている Vim で何とかできないかと思い調べたところ、そこそこ良さ気な環境を構築できたので紹介します。

使用するプラグイン

以下の2つをインストールします。NeoBundle のようなパッケージマネージャを使用するのをおすすめします。

• jvoorhis/coq.vim
• vim-scripts/CoqIDE

jvoorhis/coq.vim は Coq のシンタックスとインデント設定を追加するためのプラグインです。 vim-scripts/CoqIDE は Vim 上で CoqIDE の動作をエミュレーションするプラグインです。内部では coqtop を使っているようです。

インストール方法

NeoBundle 'jvoorhis/coq.vim'
NeoBundleLazy 'vim-scripts/CoqIDE', {
\ 'autoload' : {
\   'filetypes' : 'coq'
\ }}

使い方

Vim で拡張子 .v のファイルを開くと自動的に色付けされるようになります。 適当に証明を書いて :CoqIDENext を実行すると、証明をひとつ進めることができます。 すると、Window が分割されて CoqIDE と同様に現在の情報が表示されるようになります。 証明をひとつ戻すには :CoqIDEUndo を使います。 :CoqIDEToCursor とするとカーソル位置まで証明を進めます。

色を変える

vim-scripts/CoqIDE のデフォルト設定では証明が済んだ部分の色はライトグリーンになっています。 これは白背景のカラースキームでは良いのですが、黒背景の場合は非常に見づらいです。 これを解決するには vimrc に下記のようにハイライト設定を書きます。

autocmd FileType coq highlight SentToCoq ctermbg=17 guibg=#000080

おわりに

Vim でも結構いい感じに Coq の環境が整えられました。 まぁ ProofGeneral と比べると (多分) 機能的に劣っているとは思いますが、どうしても Vim で証明したい人は試してみてはいかがでしょうか？