Closed XVilka closed 11 months ago
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.
Is there a repro of the tree-sitter-lean
issues?
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).
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)
(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!)
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
It would be awesome to extract (if necessary) and test/integrate it with the nvim-treesitter: