Rocq (formerly Coq) grammar for tree-sitter.
The grammar is modeled around concepts from the Software Foundations (SF) Series.
- Rocq's custom
Notationsystem makes 100% static syntax coverage practically impossible (see the official reference manual). - The scope focuses on constructs encountered during practical study rather than exhaustive language coverage.
- The main purpose is to enable syntax highlighting using Tree-sitter queries.
Note
This project is experimental and actively evolving, so breaking changes may happen between commits.
The current grammar generates a solid CST for features covered in Software Foundations, Volume 1 (Logical Foundations).
As I work through Volume 2 (Programming Language Foundations), I consult the reference manual and add rules for new language features as I encounter them.
If you're using Neovim, you can install and configure this parser using nvim-tree-sitter. For other editors, consult the Tree-sitter documentation.
To see an example of the highlight groups in action, check out my personal Neovim configuration.
Even though the rules are based on the official ones, most have minor workarounds due to Tree-sitter's limitations (e.g., its one-token-lookahead nature or the restriction on matching empty strings). Plus, several (hidden) rules were added to improve maintainability and readability. The most notable cases are shown below.
| Feature / Rule | Missing Feature | Incomplete | Custom | Notes and Refs |
|---|---|---|---|---|
Coercion |
● | Only the coercion_class variant is implemented (ref). |
||
_def_body |
● | Missing reduce (ref). |
||
Inductive |
● | Missing record_definition variant and cumul_univ_decl (ref). |
||
Arguments |
● | ref. | ||
Module |
● | ref. | ||
binder |
● | Missing generalizing_binder (ref). |
||
ident_decl |
● | Missing univ_decl (ref). |
||
assert |
● | Uses a variant of as_ipat. | ||
in_clause |
● | Variant of occurrences. | ||
as_clause |
● | Variant of as_ipat. | ||
intro_pattern |
● | Variant of intropattern. | ||
pattern |
● | ref. | ||
term |
● | ref. | ||
| Tactics, Tacticals, and Ltac | ● | Uses a generalized tactic rule; tacticals support a minimal set (repeat, try); ltac is defined in terms of _ltac_expr rule (ref). |
||
Hint |
● | Uses a generalized version of the official rule. | ||
evaluation_command |
● | Uses a unified rule to cover Check, Compute, Print, Search, and Locate. |
||
_qualid_annotated |
● | Missing univ_annot (ref). |
Evalcommand hasn't been implemented (ref.).
While Coqtail syntax highlighting has been around for years, this project is meant to build on top of the existing ecosystem.
I used Coqtail for a while, but its reliance on heavy Vim script regex noticeably slowed down my editor—even when just typing whitespace.
Other alternatives like the official VS Code extension don't quite deliver a rich syntax highlighting experience compared to other languages (not to mention it's built for VS Code, and colors look a bit flat). Meanwhile, plugins like vsrocq.nvim leave out syntax highlighting.
While syntax highlighting is the main focus, having a concrete CST opens up a lot of other possibilities (like custom text-objects, code folding, and structural navigation).
If you're curious about what else you can do with a Tree-sitter parser, check out this Medium post for some great examples.
- Rocq Reference Manual —Primary reference for language syntax.
- Tree-sitter —The parser generator.
- nvim-tree-sitter —Neovim integration.
Everything is welcome :].