Closed7
Coq を Neovim から触ってみる
タイトル通り。
環境は以下の通り。
- NVIM v0.8.1
- dein 3.0
- python 3.10.8
- Coq 8.16.1
- OCaml 4.10.2
基本的に Coq は ProofGeneral (Emacs) か、CoqIDE を使うのが良いとされているが、宗教上の理由により、なんとか neovim でやっていきたい。
https://github.com/whonore/Coqtail を使うのが良さそうなので、適当に追加する。
そうすると、問題なく入るのだが、README にあるコマンドが動かない。
:CoqStart
ここでしばらく詰まっていたが、なんとなく直感で以下のコマンドを打ってみると動いた。
:call coqtail#start()
なんとなく、dein の辺りでもこの辺の話があったような気がするが、詳しいことはわかっていない。
と、思っていたが、ディレクトリを変えて、別プロジェクトにして、色々入れ直したらなんか動いた。
バージョンとかは変わっていないはずだが……
とにかく動いたのでヨシ!
ひとまず
let mapleader = "\<Space>"
として、leader を変更
流石に\
は打ちにくい
追記
と思っていたが、普通にこれをやるとインサートモードでもスペースの度に少しラグが入るようになり、最悪だったのでやめた
更に追記
とは言え、あまりにも体験が悪いし、結局このままだと\
を打つ度にラグが入り気持ち悪い
ので、以下の設定を書いた
[[plugins]]
repo = 'whonore/Coqtail'
hook_add = '''
let g:coqtail_nomap = 1
nmap <Space> [coqtail]
nnoremap <silent> [coqtail]cc <Plug>CoqStart
nnoremap <silent> [coqtail]cq <Plug>CoqStop
nnoremap <silent> [coqtail]cj <Plug>CoqNext
nnoremap <silent> [coqtail]ck <Plug>CoqUndo
nnoremap <silent> [coqtail]cn <Plug>CoqToLine
nnoremap <silent> [coqtail]cT <Plug>CoqToTop
nnoremap <silent> [coqtail]cG <Plug>CoqJumpToEnd
nnoremap <silent> [coqtail]cE <Plug>CoqJumpToError
'''
しばらく sf を進めていたら、やっぱり補完が欲しくなってきた。
LSP 自体はありそうだが……
lsp も入れた
設定は以下
local configs = require'lspconfig/configs'
configs.coqlsp = {
default_config = {
cmd = {'coq-lsp', '--std'};
filetypes = {'coq'};
root_dir = function(fname)
return lspconfig.util.find_git_ancestor(fname) or vim.loop.os_homedir()
end;
settings = {};
};
}
ただ、動いているかというと……?
エラーは出ていないが、ちゃんと LSP が起動しているのか怪しい
何やらログファイルは吐いているが
root_dir
の辺りが怪しいか
記載が古いので一旦クローズ
dein はやめて Lazy にしているが、Coq はあまり書いていない
このスクラップは2ヶ月前にクローズされました