vscoq.nvim

A Neovim client for VsCoq 2 vscoqtop.

Prerequisites

• Latest stable version of Neovim
• vscoqtop

Setup

vim-plug

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()

lazy.nvim

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

Interface

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

Configurations

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

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

Basic LSP configuration

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

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

Key	Type	Default value	Description
lsp.cmd	string[]	{ "vscoqtop" }	Path to vscoqtop (e.g. path/to/vscoq/bin/vscoqtop) and arguments passed
lsp.trace	"off" | "messages" | "verbose"	"off"	Toggles the tracing of communications between the server and client

Memory management (since >= vscoq 2.1.7)

Key	Type	Default value	Description
vscoq.memory.limit	int	4	specifies the memory limit (in Gb) over which when a user closes a tab, the corresponding document state is discarded in the server to free up memory

Goal and info view panel

Key	Type	Default value	Description
vscoq.goals.diff.mode	"on" | "off" | "removed"	"off"	Toggles diff mode. If set to removed, only removed characters are shown
vscoq.goals.messages.full	bool	false	A toggle to include warnings and errors in the proof view
vscoq.goals.maxDepth	int	17	A setting to determine at which point the goal display starts eliding (since version >= 2.1.7 of vscoqtop)

Proof checking

Key	Type	Default value	Description
vscoq.proof.mode	"Continuous" | "Manual"	"Manual"	Decide whether documents should checked continuously or using the classic navigation commmands (defaults to Manual)
vscoq.proof.pointInterpretationMode	"Cursor" | "NextCommand"	"Cursor"	Determines the point to which the proof should be check to when using the 'Interpret to point' command
vscoq.proof.cursor.sticky	bool	true	A toggle to specify whether the cursor should move as Coq interactively navigates a document (step forward, backward, etc...)
vscoq.proof.delegation	"None" | "Skip" | "Delegate"	"None"	Decides which delegation strategy should be used by the server. Skip allows to skip proofs which are out of focus and should be used in manual mode. Delegate allocates a settable amount of workers to delegate proofs
vscoq.proof.workers	int	1	Determines how many workers should be used for proof checking
vscoq.proof.block	bool	true	Determines if the the execution of a document should halt on first error (since version >= 2.1.7 of vscoqtop)

Code completion (experimental)

Key	Type	Default value	Description
vscoq.completion.enable	bool	false	Toggle code completion
vscoq.completion.algorithm	"StructuredSplitUnification" | "SplitTypeIntersection"	"SplitTypeIntersection"	Which completion algorithm to use
vscoq.completion.unificationLimit	int (minimum 0)	100	Sets the limit for how many theorems unification is attempted

Diagnostics

Key	Type	Default value	Description
vscoq.diagnostics.full	bool	false	Toggles the printing of Info level diagnostics

Example:

require'vscoq'.setup {
  vscoq = {
    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>VsCoq stepForward<CR>', { buffer = bufnr, desc='VsCoq step forward' })
      vim.keymap.set({ 'n', 'i' }, '<C-M-k>', '<Cmd>VsCoq stepBackward<CR>', { buffer = bufnr, desc='VsCoq step backward' })
      vim.keymap.set({ 'n', 'i' }, '<C-M-l>', '<Cmd>VsCoq interpretToPoint<CR>', { buffer = bufnr, desc='VsCoq interpret to point' })
      vim.keymap.set({ 'n', 'i' }, '<C-M-G>', '<Cmd>VsCoq interpretToEnd<CR>', { buffer = bufnr, desc = 'VsCoq interpret to end' })
    end,
    -- autostart = false, -- use this if you want to manually `:LspStart vscoqtop`.
    -- cmd = { 'vscoqtop', '-bt', '-vscoq-d', 'all' }, -- for debugging the server
  },
}

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

Features not implemented yet

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

See also

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