Home

Awesome

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 Pure Lua

More details at the PERFORMANCE.md

Features

Note: Due to compression, reality is faster than gifs

Fast as fuck

Fuzzy Search

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

fuzz_search.img

Preview

doc_popup.img

LSP

lsp_imports.img

lsp_snippets.img

Install the Nvim Official LSP integration

Requires 2 lines of change to support LSP snippets

local lsp = require "lspconfig"
local coq = require "coq" -- add this

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

Snippets

snippet_norm.img

snippet_expand.img

snip_load.img

The % statistic comes from compiling the 10,000 snippets

TreeSitter

treesitter.img

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 a limited number of lines about the cursor and only on Idle events due to unrealized performance promises.

CTags

ctags.img

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

Paths

paths.img

Buffers

buffers.img

Registers

Tmux

tmux.img

Tabnine

tabnine.img

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

Modular lua sources & external third party integrations

repl.img

Shown above: shell repl.

Some other built-ins:

Statistics

:COQstats

statistics.img

Validating config parser

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

conf_demo.img

Pretty

pretty.gif

If you can't see icons properly:

Either set let g:coq_settings = { 'display.icons.mode': 'none' } to disable icons, or install a supported font

Install

Windows requires symlinks support in git.

git config --global core.symlinks true

Needs python virtual env

apt install --yes -- python3-venv

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

<details> <summary>Vim</summary>

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'}

" lua & third party sources -- See https://github.com/ms-jpq/coq.thirdparty
" Need to **configure separately**

Plug 'ms-jpq/coq.thirdparty', {'branch': '3p'}
" - shell repl
" - nvim lua api
" - scientific calculator
" - comment banner
" - etc
</details> <details> <summary>Neovim</summary>

lazy.nvim

{
  "neovim/nvim-lspconfig", -- REQUIRED: for native Neovim LSP integration
  lazy = false, -- REQUIRED: tell lazy.nvim to start this plugin at startup
  dependencies = {
    -- main one
    { "ms-jpq/coq_nvim", branch = "coq" },

    -- 9000+ Snippets
    { "ms-jpq/coq.artifacts", branch = "artifacts" },

    -- lua & third party sources -- See https://github.com/ms-jpq/coq.thirdparty
    -- Need to **configure separately**
    { 'ms-jpq/coq.thirdparty', branch = "3p" }
    -- - shell repl
    -- - nvim lua api
    -- - scientific calculator
    -- - comment banner
    -- - etc
  },
  init = function()
    vim.g.coq_settings = {
        auto_start = true, -- if you want to start COQ at startup
        -- Your COQ settings here
    }
  end,
  config = function()
    -- Your LSP settings here
  end,
}
</details>

Documentation

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]

FAQ

Default hotkeys?

Always:

keyfunction
<c-space>manual completion
<c-h>edit snippet placeholder

When completion menu is open:

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

Unbound:

keymapfunction
coq_settings.keymap.repeatrepeat last edit
coq_settings.keymap.eval_snipsevulate snippet in document / under selection

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

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

. Repeat

Set coq_settings.keymap.repeat to a hotkey.

See :COQhelp keybind for details

Flickering

By default, the old results are cleared on each keystroke, so the popup menu is closed right away.

You can disable this: at the cost of having stale results shown until the new ones come in.

let g:coq_settings = { 'display.pum.fast_close': v:false }

This is not the default because some LSP servers are very slow (ie. tailwindcss), leading to stale results being shown for too long.

Autostart COQ

let g:coq_settings = { 'auto_start': v:true } or let g:coq_settings = { 'auto_start': 'shut-up' }

This must be set BEFORE require("coq")

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.

LSP sometimes not importing

Increase coq_settings.clients.lsp.resolve_timeout

This will however, make applying edits slower.

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.

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>

If you like this...

Also check out

Special Thanks & Acknowledgements

The snippets are compiled from the following open source projects:

Super special thanks goes to Typescript LSP.

Nothing like good motivation to improve my design than dumping 1000 results on my client every other keystroke.