nvim-treesitter: upstream Tree-Sitter grammar and queries about lean.nvim HOT 6 CLOSED

Hey! The parser is already extracted here -- but ran into quite crippling tree-sitter issues with the size of the grammar. The queries that are in this repo could indeed be upstreamed, but I'm not really working on tree-sitter related support anymore until/unless the issues with tree-sitter-lean are resolved. We anyways have semantic highlighting now in Lean's LSP, so there's slightly less of an incentive.

from lean.nvim.

The relevant (or at least what I recall was seemingly relevant sounding to me) upstream issue is tree-sitter/tree-sitter#693 (or tree-sitter/tree-sitter#1041)

from lean.nvim.

Essentially simply try to build the repo using tree-sitter generate -- two things will happen -- it will take ages, and then also will produce a giant parser (.c file -- one that actually exceeds the GitHub size limits now for committing a file to a repository).

from lean.nvim.

This is off-topic, I know, but there are ways of keeping the parser size in check by being smarter about writing the grammar (which is an art, not a science). Some tips can be found here: https://github.com/tree-sitter/tree-sitter/wiki/Tips-and-Tricks-for-a-grammar-author

from lean.nvim.

Is there a repro of the tree-sitter-lean issues?

from lean.nvim.

(I'm going to close this I think since I'm not sure there's anything to do in this repo specifically, but I'd be very glad for help if anyone is interested in it -- feel free to send whatever advice, PRs, or issues to the tree-sitter-lean repo!)

from lean.nvim.