`_dollar` seems to cause the grammar to explode

[vigoux]

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]

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]

(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]

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]

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

That would be hugely appreciated!