search

Julian / tree-sitter-lean

Experimental tree-sitter parser for the Lean (4) Theorem Prover
MIT License
28 stars 5 forks source link

`_dollar` seems to cause the grammar to explode #5

Open vigoux opened 10 months ago

vigoux commented 10 months ago

DISCLAIMER: I am not a lean expert, I just started to learn it.

I was debugging a little the reason why the grammar was extremely long to generate, despite not being that big. For that I followed the steps mentioned in this wiki page.

It seems that the _dollar rule causes a lot of states to be generated, and that could be the source of the issues.

Here are the top offenders in terms of state counts:

binary_expression               12424
comparison                      9877
_dollar                         9877
subarray                        9664
let                             6881
match                           2301
tactics                         1756
tactics_repeat1                 1620
fun_repeat2                     1557
fun                             1305
_do_seq_repeat1                 1246
_do_seq                         1136

I would very much like to help, but I do not have enough lean knowledge to provide any meaningful fix at the moment.

Julian commented 10 months ago

Hey! Thanks for the drive by :) (I think we've interacted at some point somewhere, but I'm sure nice to meet you)

On the substance of your tip -- I think I've seen earlier versions of that page and tried to dig in here and basically follow it, but not really been successfully, especially considering that sometimes some movement in the opposite direction (getting bigger) is temporarily needed to refactor into something smaller...

I don't yet have much appetite to get back into trying to fix this even if it is possible, but thanks for sharing the reference in the event I do get back to things.

Julian commented 10 months ago

(I should say -- work on this repo got a lot less "urgent" once it was clear semantic highlighting support was going to be merged in nvim...)

vigoux commented 10 months ago

Regarding the "semantic" highlighting part, as of my current setup with lean in neovim, the semantic highlighting implemented in the Lean LSP implementation (or at least my version, which is version 4.1.0) is lacking a lot of things (like strings, numbers, types, ...).

Thus having a "sane fallback" is greatly appreciated.

I have been practicing with Lean4 lately, so I'll try to come up with a meaningful contribution.

Julian commented 10 months ago

I have been practicing with Lean4 lately, so I'll try to come up with a meaningful contribution.

That would be hugely appreciated!