Neovim Setup¶

This guide covers setting up Prove in Neovim with syntax highlighting (tree-sitter) and language server (LSP).

Prerequisites¶

• Neovim 0.10+
• Python 3.11+
• gcc/clang for building tree-sitter parser

Install Prove¶

pip install -e "prove-py/[dev]"

ML completion stores are downloaded automatically to ~/.prove/ the first time the LSP starts.

Tree-Sitter Setup¶

Option 1: Using nvim-treesitter (Recommended)¶

NvChad users and those with nvim-treesitter already configured:

1. Add to your nvim-treesitter config:

require("nvim-treesitter.install").compilers = { "clang", "gcc" }

require("nvim-treesitter.configs").setup({
  ensure_installed = {
    -- other parsers
    "prove",
  },
  highlight = {
    enable = true,
  },
})

1. Add filetype detection:

vim.filetype.add({
  extension = {
    prv = "prove",
    intent = "prove",
  },
})

1. Force-load the parser (if not auto-detected):

pcall(vim.treesitter.language.add, "prove", {
  path = vim.fn.stdpath("data") .. "/lazy/nvim-treesitter/parser/prove.so",
})

Option 2: Manual Installation¶

Build and install the parser manually:

cd tree-sitter-prove
npm install
npm run build

Then symlink the parser:

mkdir -p ~/.local/share/nvim/site/pack/vendor/start/nvim-treesitter/parser
ln -s ~/Projects/prove/tree-sitter-prove/parser/prove.so \
  ~/.local/share/nvim/site/pack/vendor/start/nvim-treesitter/parser/prove.so

LSP Setup (proof lsp)¶

Prove includes an LSP server for diagnostics, code completion, and go-to-definition.

Option 1: NvChad / nvim-lspconfig¶

Add this to your LSP config (lua/configs/lspconfig.lua):

vim.api.nvim_create_autocmd("FileType", {
  pattern = "prove",
  callback = function()
    vim.lsp.start({
      name = "proof-lsp",
      cmd = { "proof", "lsp" },
      root_dir = vim.fs.root(0, { "prove.toml", ".git" }),
    })
  end,
})

The LSP will start automatically when opening .prv files.

Option 2: Manual LSP Config¶

local lspconfig = require("lspconfig")

lspconfig.prove_lsp = {
  cmd = { "proof", "lsp" },
  filetypes = { "prove" },
  root_dir = function(fname)
    return vim.fs.root(fname, { "prove.toml", ".git" })
  end,
}

lspconfig.prove_lsp.setup({})

Verify LSP is Running¶

Open a .prv file and run:

:LspInfo

You should see proof-lsp listed as an active client.

Formatting¶

Use the Prove CLI for formatting:

:!proof format %

Or configure conform.nvim / null-ls:

require("conform.nvim").setup({
  formatters_by_ft = {
    prove = { "proof" },
  },
})

With prove formatter defined as:

formatters = {
  proof = {
    command = "proof",
    args = { "--stdin-filename", "$FILENAME", "format", "-" },
    stdin = true,
  },
}

Syntax Highlighting Queries¶

Prove's tree-sitter queries are in tree-sitter-prove/queries/prove/:

• highlights.scm — syntax highlighting
• locals.scm — scope-local variables
• tags.scm — ctags support

These are automatically loaded when using nvim-treesitter.

Verify Your Setup¶

1. Open a .prv file:

nvim hello.prv

1. Check tree-sitter is active:

:TSInspect

1. Check LSP diagnostics:

:Trouble

Troubleshooting¶

Parser not loading¶

Ensure the parser file exists:

ls ~/.local/share/nvim/lazy/nvim-treesitter/parser/prove.so

If missing, rebuild:

cd tree-sitter-prove
npm run build

LSP not starting¶

Check proof is installed and on your $PATH:

which proof
proof lsp --help

If not found, build proof first: python -m prove build proof/ and add the output directory to $PATH. If ML completions are missing or broken, run prove setup to force a re-download of the stores.

No syntax highlighting¶

Force reload:

:edit!
:TSUpdateSync prove