Lean4

[femtomc]

Check for existing issues

• [X] Completed

Language

Lean4

Tree Sitter parser link

https://github.com/Julian/tree-sitter-lean

Language server link

https://github.com/leanprover/lean4/tree/master/src/Lean/Server

Misc notes

There's also a React app to support the Infoview window: https://www.npmjs.com/package/@leanprover/infoview

[uargos]

@femtomc are you working on an implementation ? I'm considering adding it myself.

[femtomc]

@uargos I am not, but would certainly benefit from one 😄

[uargos]

Ok. I'll give it a try !

[uargos]

Status:

I spent some time trying to plug inlay hints, without noticing that inlay hints had not reached stable on the lean lsp (see zed-industries/zed#24401) 🙄 On nightly, all the lsp support works out of the box and is pretty good imo.

I plugged https://github.com/Julian/tree-sitter-lean but there are a lot of parse errors. This is probably due to (among other things), the fact that the syntax of lean is essentially built around dynamic syntax extensions (aiming to support arbitrary dsls ...). Since afaict in zed the tree-sitter grammar is mainly used for syntax coloring, I'll probably rewrite a simpler but less brittle grammar covering the special cases.

I have not looked at the infoview thing yet, but I don't think it will be simple to plug. We'll see.

[blackbird314]

@uargos

Hi, how about the progress of tree-sitter-lean? I made a lean4 zed extension but the current tree-sitter is not ideal.

[uargos]

@blackbird314

Hey, I gave a few tries to implementing a proper tree-sitter parser, but was out of luck getting something to work. I kind of got lost in the code of the lean parser when trying to translate it to the tree-sitter framework. Since the lean parser is supposed to support arbitrary syntax extensions, it is not the simplest to translate.

I probably don't know enough of Lean and tree-sitter to make that work over a few sessions.

Edit:

The best solution would probably to support semantics token from the language server.

[drdozer]

I would love good lean4 support within zed, supporting a similar interactive environment to that in vs code. I hate to be that person, but have you tried a modern agentic coder to build some of the translations and glue? It's the sort of thing they seem to be quite good at particularly if you can get them to incrementally check their work against a library of test cases.

[uargos]

I tried a few times yes, with different approaches. None of them worked.

[lnay]

I dug a bit into this topic today. What I found is that the infoview is only part of the issue here (which on its own could be possible in an external window if you built a process in the middle of zed and the lean4 language server).

The lean4 language server expects the LSP spec to be violated for specific messages and really needs non-standard messages for more than just the infoview.

My takeaway was that there's little point pursuing this seriously before extensions have the ability to provide hooks for certain buffer events and send custom LSP messages. No amount of workarounds with extra language server shims is going to get around this.

[lnay]

Relevant conversation (involving a zed team member too): https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/Lean.20.2B.20Zed.20integration/near/505671509