Zenn
Open6

Coq を Neovim から触ってみる

Neovim
coq
lmdexprlmdexpr

タイトル通り。

環境は以下の通り。

  • NVIM v0.8.1
    • dein 3.0
  • python 3.10.8
  • Coq 8.16.1
  • OCaml 4.10.2
lmdexprlmdexpr

基本的に Coq は ProofGeneral (Emacs) か、CoqIDE を使うのが良いとされているが、宗教上の理由により、なんとか neovim でやっていきたい。
https://github.com/whonore/Coqtail を使うのが良さそうなので、適当に追加する。

そうすると、問題なく入るのだが、README にあるコマンドが動かない。

:CoqStart

ここでしばらく詰まっていたが、なんとなく直感で以下のコマンドを打ってみると動いた。

:call coqtail#start()

なんとなく、dein の辺りでもこの辺の話があったような気がするが、詳しいことはわかっていない。

lmdexprlmdexpr

と、思っていたが、ディレクトリを変えて、別プロジェクトにして、色々入れ直したらなんか動いた。
バージョンとかは変わっていないはずだが……
とにかく動いたのでヨシ！

lmdexprlmdexpr

ひとまず

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
'''
lmdexprlmdexpr

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の辺りが怪しいか