A Neovim client for VsRocq vsroqtop.

• Latest stable version of Neovim
• vsrocqtop

Plug 'whonore/Coqtail' " for ftdetect, syntax, basic ftplugin, etc
Plug 'tomtomjhj/vsrocq.nvim'

...

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

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

{
  'whonore/Coqtail',
  init = function()
      vim.g.loaded_coqtail = 1
      vim.g["coqtail#supported"] = 0
  end,
},
{
  'tomtomjhj/vsrocq.nvim',
  filetypes = 'coq',
  dependecies = {
    'whonore/Coqtail',
  },
  opts = {
    vsrocq = { ... }
    lsp = { ... }
  },
},

• vsrocq.nvim uses Neovim's built-in LSP client and nvim-lspconfig. See kickstart.nvim for basic example configurations for working with LSP.
• :VsRocq command
  • :VsRocq continuous: Use the "Continuous" proof mode. It shows goals for the cursor position.
  • :VsRocq manual: Use the "Manual" proof mode (default), where the following four commands are used for navigation.
    • :VsRocq stepForward
    • :VsRocq stepBackward
    • :VsRocq interpretToEnd
    • :VsRocq interpretToPoint
  • :VsRocq panels: Open the proofview panel and query panel.
  • Queries
    • :VsRocq search {pattern}
    • :VsRocq about {pattern}
    • :VsRocq check {pattern}
    • :VsRocq print {pattern}
    • :VsRocq locate {pattern}
  • Proofview
    • :VsRocq admitted: Show the admitted goals.
    • :VsRocq shelved: Show the shelved goals.
    • :VsRocq goals: Show the normal goals and messages (default).
  • etc
    • :VsRocq jumpToEnd: Jump to the end of the checked region.

The setup() function takes a table with the followings keys:

• vsrocq: Settings specific to VsRocq, used in both the client and the server. This corresponds to the "configuration" key in VsRocq's package.json.
• lsp: The settings forwarded to :help lspconfig-setup. :help vim.lsp.ClientConfig.

Some settings in VsRocq's package.json should be configured in nvim's LSP client configuration:

• "vsrocq.path" and "vsrocq.args" → lsp.cmd
• "vsrocq.trace.server" → lsp.trace

require'vsrocq'.setup {
  vsrocq = {
    proof = {
      -- In manual mode, don't move the cursor when stepping forward/backward a command
      cursor = { sticky = false },
    },
  },
  lsp = {
    on_attach = function(client, bufnr)
      -- your mappings, etc

      -- In manual mode, use ctrl-alt-{j,k,l} to step.
      vim.keymap.set({ 'n', 'i' }, '<C-M-j>', '<Cmd>VsRocq stepForward<CR>', { buffer = bufnr, desc='VsRocq step forward' })
      vim.keymap.set({ 'n', 'i' }, '<C-M-k>', '<Cmd>VsRocq stepBackward<CR>', { buffer = bufnr, desc='VsRocq step backward' })
      vim.keymap.set({ 'n', 'i' }, '<C-M-l>', '<Cmd>VsRocq interpretToPoint<CR>', { buffer = bufnr, desc='VsRocq interpret to point' })
      vim.keymap.set({ 'n', 'i' }, '<C-M-G>', '<Cmd>VsRocq interpretToEnd<CR>', { buffer = bufnr, desc = 'VsRocq interpret to end' })
    end,
    -- autostart = false, -- use this if you want to manually `:LspStart vscoqtop`.
    -- cmd = { 'vsrocqtop', '-bt', '-vsrocq-d', 'all' }, -- for debugging the server
  },
}

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

• Fancy proofview rendering
  • proof diff highlights
• Make lspconfig optional

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