feat(languages): Lean experimental tree-sitter-lean

[Anderssorby]

Trying out the experimental tree-sitter-lean from @Julian

[Julian]

Cool :) Let me know how it goes. There are lots of issues (and in neovim it's super painful perf wise at the minute because the queries are large), but it does work.

[Anderssorby]

BTW is the parser the C output of the compiled Lean parser? And would it make sense to rather use the Lean source for compiling this? I've been making several Lean <-> C <-> Rust bindings.

[Julian]

BTW is the parser the C output of the compiled Lean parser?

It's what tree-sitter emits from the compiled typescript Lean parser if that's what you mean.

And would it make sense to rather use the Lean source for compiling this?

The grammar was mostly hand-ported (first not-very-directly, now somewhat directly) from the Lean source. It did (does) occur to me that it may be possible to transpile it but I haven't experimented with doing so.

[Anderssorby]

Currently the syntax highlight only works when there is an error. The LSP works fine, but it needs to have some display of the '$/lean/fileProgress' notification (which I'm guessing is the goal view).

[Julian]

fileProgress is Lean (server) saying what parts of the file it's processing. The infoview stuff is pulled by the client. In neovim this lives here: https://github.com/Julian/lean.nvim/blob/main/lua/lean/rpc.lua#L238-L281 and is done via the RPC protocol. (Neither of those should have much to do with syntax highlighting I think? But I don't know anything about Helix :) maybe I should try it.)

[the-mikedavis]

in neovim it's super painful perf wise at the minute because the queries are large

I think this should be improved with tree-sitter v0.20.2 (see tree-sitter/tree-sitter#1510), but I'm not sure if dependabot has ugraded that dependency yet in helix

[Julian]

Yes! Indeed that change fixed the perf issue on the neovim side.

[archseer]

0.20.2 is in master, but I've accidentally excluded it from the 0.6 release. I'll push a patch release later this week to include some bug fixes so it'll be included in a stable release then as well.

[Anderssorby]

So do you want to merge this? It works for me although more features could be added like a lean info view.

[archseer]

I'll do a thorough review later today, but as mentioned on Matrix, the highlights need to be modified to match https://docs.helix-editor.com/themes.html#syntax-highlighting

There's no @number for example, we use @constant.numeric.integer

Similarly the injections.scm definitions are different

[Anderssorby]

@archseer Are we okay for merging? I'll probably add an Lean info view in a later PR.

[the-mikedavis]

I think you'll want to move this stanza down to the bottom of the file. The higher in the file, the higher the precedence with helix (it's reversed in neovim), so this stanza will match all identifiers and so the rules on L38-L67 will never match.

[Anderssorby]

I notice that there are still several bugs in the highlightning, but this is probably an error in the lean-tree-sitter parser and not here.

Seems like def, for, partial, open, end and more fails to parse correctly sometimes. Lean4 is still experimental and the syntax keeps getting updated so I think it should be okay to merge before things are perfect.
@Julian

[Julian]

Yes, there are still plenty of parsing bugs. Issues or patches are of course welcome.

[Anderssorby]

@the-mikedavis So let's merge?

[archseer]

Sorry for the delay, I'll merge after the CI run 👍🏻

[archseer]

Probably not the best place to raise this, but @Julian any idea why the compiled Lean grammar is so big? It's 16MB, compared to haskell's 3.2MB or rust's 1.1MB.

[Julian]

It's a big/complicated grammar -- IIRC Agda's is similarly large and ran into some of the same tree-sitter issues I ran into. There's some improvements possible but right now improving it has been somewhat low priority for me in favor of other Lean editor things (and other obligations entirely). PRs certainly welcome.