coq.nvim 🐔

Named after the famous theorem prover

coq also means in français québécois, and I guess 🥖.

Fast as FUCK and loads of features.

Faster Than Lua

  • Native C in-memory B-trees

  • SQLite VM interrupts

  • Coroutine based incremental & interruptible scheduler

  • TCP-esque flow control

More details at the


Note: Due to compression, reality is faster than gifs

Fast as fuck

  • Results on every keystroke

  • Throttling? Never heard of her

  • Real time performance statistics

  • Look at the gifs! The bottom few are the fastest when I didn't show down on purpose to show features.

Fuzzy Search

Error correction: cour -> colour_space, flgr -> flag_group, nasp -> Namespace



  • Press key to view documentation in big buffer

  • Auto open preview on side with most space

  • Customizable location: n, s, w, e

  • Ubiquitous: Tags, LSP, Paths, Snippets



  • Incremental completion

  • Client-side caching

  • Multi-server completion (i.e. tailwind + cssls)

  • Header imports


  • Snippet Support


Install the Nvim Official LSP integration

Requires 1 line of change to support LSP snippets

local lsp = require "lspconfig"

lsp.<server>.setup(<stuff...>)                              -- before
lsp.<server>.setup(coq.lsp_ensure_capabilities(<stuff...>)) -- after

If you are using packer.nvim

vim.schedule(function ()
  local lsp = require "lspconfig"
  require("packer").loader("coq_nvim coq.artifacts")



  • Linked regions


The % statistic comes from compiling the 10,000 snippets

See FAQ to see limitations due to upstream bug


  • Incremental & automatic background compilation

  • Tag location & context

  • Non-blocking


Requires Universal CTags, NOT ctags

# MacOS
brew uninstall ctags           # bad
brew install   universal-ctags # good

# Ubuntu
apt remove  ctags              # bad
apt install universal-ctags    # good


  • Preview contents

  • Relative to both cwd and file path



  • Real time completion

  • Fast in files with thousands of lines



  • Unicode ready

  • I don't have a picture, it's boring

Treesitter is still unstable in nvim0.5: slow and crash prone

The promise is that Treesitter will have real time parsing on every keystroke, but it's actually too slow on big files.

The Treesitter source only parses on Idle events due to unrealized performance promises.




  • CPU preserving flow control

  • Auto download & install & update


T9 is disabled by default, I might remove it, if they do not improve the CPU usage. Their own bug tracker.

Enable via: coq_settings.clients.tabnine.enabled=true




Validating config parser

  • Prevents typos & type errors in your config

Here I make a type error on purpose inputting string instead of an integer.



Needs python virtual env

apt install --yes -- python3-venv

Minimum version: python:3.8.2, nvim: 0.5, sqlite: recentish

Install the usual way, ie. VimPlug, Vundle, etc

" main one
Plug 'ms-jpq/coq_nvim', {'branch': 'coq'}
" 9000+ Snippets
Plug 'ms-jpq/coq.artifacts', {'branch': 'artifacts'}
-- packer
use { 'ms-jpq/coq_nvim', branch = 'coq'} -- main one
use { 'ms-jpq/coq.artifacts', branch= 'artifacts'} -- 9000+ Snippets


To start coq

" the [-s, --shut-up] flag will remove the greeting message
:COQnow [--shut-up]

🌟 If required, it will ask you to run :COQdeps, please run it and do :COQnow again.

There is built-in help command

:COQhelp [--web] [topic]


Default hotkeys?


key function
<c-space> manual completion
<c-h> edit snippet placeholder

When completion menu is open:

key function
<c-k> move preview to bigger window
<esc> exit to normal
<backspace> backspace
<enter> select completion
<tab> next result
<s-tab> prev result

When hovering over a result, entering any key [a-z] will select it

This is a vim thing, I have zero control over :(

Autostart COQ

let g:coq_settings = { 'auto_start': v:true } (or the lua way)

LSP too slow to show up on keystroke.

You have some options, each has its trade off:

  1. Increase the coq_settings.limits.completion_auto_timeout.

This will slow down feedback on every keystroke, as coq waits for LSP.

  1. Use the manual completion hotkey (default <c-space>)

Annoying! And the manual completion also has a timeout coq_settings.limits.completion_manual_timeout.

Some LSP servers will still fail to respond within the default .66 seconds, in that case pressing <c-space> multiple times might actually help some LSP servers catch up, depending on their implementation.

Missing Results

On keystroke only a max of coq_settings.match.max_results are shown.

Use manual completion hotkey to show all results.

Some LSP servers give inconsistent completions

This happens when certain LSP servers give you 1000s of unfiltered results in alphabetical order and you still have to respond in a few dozen milliseconds.

To eliminate a-z bias, coq does a random sort on the resultset and process and cache as many of them as possible within the performance window.

So if some results are not in the SQLite cache, and have yet to be processed, they will be missing. They might however still show up on later keystrokes.

Use the manual hotkey if you need to see everything.

Auto completion mess up snippet regions (the ones you can jump to)

This is an upstream nvim issue.

Theoretically I can work around this by writing my own nvim extmark reconciliator, or I can go and cuddle my puppy and let upstream fix it.

My vim crashed!

Disable TreeSitter

Treesitter still needs stability work.

I want to use a different python version

vim.g.python3_host_prog=<absolute path to python>

Note: ~/ will not be expanded to $HOME, use vim.env.HOME .. <path> (lua) or $HOME . <path> (viml) instead.