coq-lsp.nvim

A simple Neovim client for coq-lsp.

Prerequisites

• Latest stable version of Neovim
• coq-lsp

Setup

Plug 'neovim/nvim-lspconfig' " only on neovim < 0.11
Plug 'whonore/Coqtail' " for ftdetect, syntax, basic ftplugin, etc
Plug 'tomtomjhj/coq-lsp.nvim'

...

" Don't load Coqtail
let g:loaded_coqtail = 1
let g:coqtail#supported = 0

" Setup coq-lsp.nvim
lua require'coq-lsp'.setup()

Interface

• coq-lsp.nvim uses Neovim's built-in LSP client and nvim-lspconfig. See kickstart.nvim for basic example configurations for working with LSP.
• On cursor movement, it asynchronously displays the goals for the position of cursor on the auxiliary panel.
• :CoqLsp command
  • :CoqLsp open_info_panel: Open the info panel for the current buffer.
  • :CoqLsp saveVo: Save the .vo file for the current buffer.
• Commands from nvim-lspconfig work as expected. For example, run :LspRestart to restart coq-lsp.

Configurations

require'coq-lsp'.setup {
  -- The configuration for coq-lsp.nvim.
  -- The following is the default configuration.
  coq_lsp_nvim = {
    --   "tab"    = one shared panel per tab, tracks the focused coq buffer.
    --   "buffer" = one panel per coq buffer.
    info_panel_mode = 'tab',
    -- If true, a manually closed panel stays closed until you explicitly
    -- reopen it with `:CoqLsp open_info_panel`.
    info_panel_sticky_close = true,
  },

  -- The configuration forwarded to `:help lspconfig-setup`.
  -- The following is an example.
  lsp = {
    on_attach = function(client, bufnr)
      -- your mappings, etc
    end,
    -- coq-lsp server initialization configurations, defined here:
    -- https://github.com/ejgallego/coq-lsp/blob/main/editor/code/src/config.ts#L3
    -- Documentations are at https://github.com/ejgallego/coq-lsp/blob/main/editor/code/package.json.
    init_options = {
      show_notices_as_diagnostics = true,
    },
    autostart = false, -- use this if you want to manually launch coq-lsp with :LspStart.
  },
}

NOTE: Do not call lspconfig.coq_lsp.setup() or vim.lsp.enable() yourself. require'coq-lsp'.setup does it for you.

Features not implemented yet

• Fancy proofview rendering

See also

• coq.ctags for go-to-definition.
• vscoq.nvim for vscoqtop client.