vscoq.nvim

A Neovim client for VsCoq 2 vscoqtop.

Prerequisites

• Latest stable version of Neovim
• vscoqtop

Setup

Plug 'neovim/nvim-lspconfig'
Plug 'whonore/Coqtail' " for ftdetect, syntax, basic ftplugin, etc
Plug 'tomtomjhj/vscoq.nvim'

...

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

" Setup vscoq.nvim
lua require'vscoq'.setup()

Interface

• vscoq.nvim uses Neovim's built-in LSP client and nvim-lspconfig. See kickstart.nvim for basic example configurations for working with LSP.
• Ex commands
  • :ToggleManual: Toggle proof mode between "Continuous" (default, show goals for the cursor position) and "Manual" modes.
  • manual mode:
    • :InterpretToPoint
    • :Forward
    • :Backward
    • :ToEnd
  • :Panels: Open the proofview panel and query panel.
  • Queries
    • :Search {pattern}
• Commands from nvim-lspconfig work as expected. For example, run :LspRestart to restart vscoqtop.

Configurations

require'vscoq'.setup {
  -- Configuration for vscoq, used in both the client and the server.
  -- See "configuration" in https://github.com/coq-community/vscoq/blob/main/client/package.json.
  -- The following is an example.
  vscoq = {
    proof = {
      mode = 0, -- manual mode
    },
  },

  -- The configuration forwarded to `:help lspconfig-setup`.
  -- The following is an example.
  lsp = {
    on_attach = function(client, bufnr)
      -- your mappings, etc
    end,
    autostart = false, -- use this if you want to manually launch vscoqtop with :LspStart.
  },
}

NOTE: Do not call lspconfig.vscoqtop.setup() yourself. require'vscoq'.setup does it for you.

Features not implmented yet

• Other queries
• Nice proofview panel

See also

• coq.ctags for go-to-definition.
• coq-lsp.nvim for coq-lsp client.