手を出したかったけど出せていなかったCoqに入門しました。
Coqの環境として、メジャーなものは以下があるようです。
- CoqIDE
- 恐らく、Coq界では標準に近い開発環境かと思います
- Arch Linuxでは
pacman -S coqideで入りました - これを使っていたのですが、自動インデント機能が見当たらなかったので、つらくなって別環境を探しはじめたのがきっかけで、この記事が生まれました
- Proof General (Emacs拡張)
- いいらしいです。
- 宗教上の理由でEmacs使えない人でも、Coq書くときは使ってる人がいる、らしいです。
- けれども、今からEmacsに入門するのも面倒なので、今回はパスしました
ということで、なんか最近、妙にイケイケなVisual Studio Codeの拡張を探してみたら、いい感じのがありました。
インストール
VSCodeの拡張機能を探すところに vscoq と打ち込むと出てくるやつを入れる。
https://github.com/siegebell/vscoq
操作方法
CoqIDEみたいに、1ステップずつコードを進めたり戻したりできます。
| 操作 | キーバインド |
|---|---|
| 1ステップ進める | Ctrl+Alt+↓(下矢印) |
| 1ステップ戻す | Ctrl+Alt+↑(上矢印) |
| カーソル位置までステップを動かす | Ctrl+Alt+→(右矢印) |
| 最後までステップを進める | Ctrl+Alt+End |
| 最初までステップを戻す | Ctrl+Alt+Home |
その他はこちらか、F1を押してCoqと入力して出てくるものをご参照下さい。
その他、VSCodeの設定
Coqの文法上、ドットを行の最後につけることが多いのですが、私の環境では、VSCodeでドットを入力すると補完候補が出て、Enterを押すとそれが入力される憂き目に遭いました。
これはとてもつらいです。
VSCodeの設定でこれを変えることができ、設定画面を「enter」で検索したら、
Editor: Accept Suggestion On Enter
という項目が見つかります。デフォルトではonになっていますが、offにすると、Enterで候補を選べなくなります。(smartでは、うまくいきませんでした)
最後に
よいCoqライフを。