tomtomjhj / coq-lsp.nvim

Neovim client for coq-lsp
MIT License
22 stars 0 forks source link

What version of coq-lsp does this plugin support? #4

Closed DieracDelta closed 1 year ago

DieracDelta commented 1 year ago

When I run this on HEAD of coq-lsp (ac2154bd0eb8668b62aacf5bdbea38540ade526f), I get a "document not ready" error.

Things I've done:

set:

    let g:loaded_coqtail = 1
    let g:coqtail#supported = 0

Then call:

    require'coq-lsp'.setup{
      lsp = {
        cmd = { "path/to/coq/binary" } -- this must be overridden for me since I'm on nix and directly sticking this in from my flake
      }
    }

Happy to provide a minimal reproducible example if helpful! I'm hoping this is an easy fix.

tomtomjhj commented 1 year ago

I use coq-lsp 0.1.7, coq 8.17.1, nvim HEAD (0.9.1 works too).

Please check if you can reproduce with coq-lsp 0.1.7 and VSCode.

DieracDelta commented 1 year ago

Thanks for the reply! I am using coq-lsp 0.1.7, coq 8.18.0 compiled with OCaml 4.14.1. I'm not able to reproduce with vscode. That is, coq-lsp works as expected in vscode.

It's worth noting the LSP appears to be functioning (e.g. the goals panel works) besides spamming the following error:

Error executing vim.schedule lua callback: ...ovimPackages/start/node-type-nvim/lua/node-type/init.lua:50: RPC[Error] code_name = unknown, code
= -32802, message = "Document is not ready"
stack traceback:
        [C]: in function 'error'
        ...ovimPackages/start/node-type-nvim/lua/node-type/init.lua:50: in function 'handler'
        ...eovim-unwrapped-0.9.1/share/nvim/runtime/lua/vim/lsp.lua:1394: in function ''
        vim/_editor.lua: in function <vim/_editor.lua:0>

when I type in an open coq file.

DieracDelta commented 1 year ago

Nevermind. It was an error in my lualine config that was causing this. I've since removed it and this plugin is working. Thanks for the responses!