Tree Sitter Grammar and Helix Editor Support

[gruhn]

Hey guys, I tried to bring editor support for Quint to my favorite editor Helix. Two days ago the pull request got merged. Getting support for a new language into Helix mainly requires two things: a language server and a Tree Sitter grammar. I'm glad the language server was already provided.

Tree sitter, if you don't know, is a framework for specifying the syntax of a programming language. Editors/IDEs only need to know how to talk to tree sitter, then they can use syntax highlighting for all languages that have a tree sitter grammar. This is in a similar spirit to the language server protocol. Except language servers would be too slow to provide syntax highlighting themselves. Tree Sitter grammars can also provide more "nuanced" syntax highlighting, because they completely define the language. Classic regex based methods usually just highlight keywords (and, or, iff, ...), but with tree sitter braced and { ... } and infix p and q could be highlighted differently for example.

Here is the (probably still quite buggy) Tree Sitter grammar I hacked together for Quint. Thanks to the detailed Language Manual this was not too hard. I was struggling quite a bit with those locally defined operators though:

var module_level = 
  var local_level1 = 
    var local_level2 = expr
    expr
  expr

I'm still not sure, I dealt with this correctly 😅

[romac]

Amazing! Will give it a try in Neovim! Another cool thing about Tree-Sitter grammars is that one can use them to build a formatter using Topiary, one of the few things left that I find myself wanting in Quint.

[gruhn]

I don’t know if you need to define custom highlight queries for use with Neovim. The default one is a bit bare bones right now. Tell me if you need help. I’m also happy to merge changes or added queries.

[bugarela]

This is funny timing, I was just starting Topiary configs for Quint this week and updated a bit the hacked-out tree-sitter grammar I wrote more than I year ago: https://github.com/informalsystems/quint/tree/gabriela/tree-sitter-quint. I'm not super great at grammars and this was a result of my first ever interaction with tree-sitter, so it's great to have someone else tackling this.

I'll try this out next week and see if I can adapt my topiary configs to this :D

Neovim is not my main editor, but I do have it wired up with my tree-sitter grammar and it seems to have worked ok in the few times I tried it.

[bugarela]

Grammar looks great! I see there are some questions in the comments, I'll try to answer them and maybe make PRs when I get a chance. I feel like you might have over-complicated the local operators a bit. I'm super grateful for this, it's so much better than my hacked version 😅!

I changed my short Topiary work to use this grammar instead of mine and pushed my progress into a fork: https://github.com/tweag/topiary/compare/main...bugarela:topiary:add-quint?expand=1

I'll open a PR on their repo once I'm happy with the formatting results.