Lean + Zed integration

Stream: general

[Dan Abramov]

I really miss using the Zed code editor, but it has no Lean plugin. I asked around and got this response from one of Zed's developers:

If they've got an LSP and tree sitter grammar (and those are sufficient to provide good support for it) we can probably sneak this one in pretty fast...

Do I understand correctly that this is not the case, and that tree sitter grammar for Lean would be impossible? Thanks!

[Marc Huisinga]

There's https://github.com/Julian/tree-sitter-lean for basic syntax highlighting (correct semantic highlighting is then provided through LSP). In VS Code we currently use a TextMate grammar for non-sematic highlighting, but I hope to move it away from that once VS Code properly supports tree sitter.
The problematic part will be getting an InfoView to work in Zed and making it compatible with our various protocol extensions, and it will probably also lack a lot of existing LSP features that are really useful when using Lean. There's also a couple of places where we deliberately violate LSP because it makes some decisions that are incompatible with theorem proving, but fortunately these violations are all compatible with the VS Code and NeoVim LSP clients.

In VS Code, we use https://www.npmjs.com/package/@leanprover/infoview, whereas NeoVim has its own implementation. The VS Code InfoView is a bit more feature-complete since it supports arbitrary widgets, though.

[Patrick Massot]

It would be really nice to try to work on the tree-sitter grammar. I will never be perfect, but there is no reason why it should be worse than TextMate.

[Julian Berman]

I think partly the issue is that VSCode doesn't yet have support for tree-sitter. That's the (hugely upvoted) https://github.com/microsoft/vscode/issues/50140

[Julian Berman]

So it's hard for me to hope others would help out there. I started a rewrite of the tree-sitter parser a few months ago but again ran into trouble with function application, so it needs more brainpower I think.

[Mikayla Maki]

:wave: hello y'all! I'm a software engineer on the Zed team and am following up from @Dan Abramov's reply on Bluesky :)

I know very little about the Lean language or how y'alls dev tools fit together, how essential is the InfoView and LSP extensions to y'alls work with Lean? We'd need to make some big changes to support UI extensions and LSP extensions. Lean might be a good test case for us to keep in mind when we start that work, but unfortunately we have quite a bit queued up ahead of it. If there's a subset of tooling we could make available in Zed, we can make it happen :)

[Julian Berman]

I think the short version is "it's absolutely essential", trying to use Lean without the infoview is kind of like trying to fly a plane with no instruments or view out the windshield.

[Damiano Testa]

... and without the infoview, the plane that you are trying to fly, does not have wings either.

[Julian Berman]

Though I'm curious -- I know nothing about Zed but I see https://zed.dev/extensions -- what's the impossible bit at the minute, an extension can't create and manage windows?

[Julian Berman]

Or make custom LSP requests it sounds like?

[Chris Bailey]

Mikayla Maki said:

:wave: hello y'all! I'm a software engineer on the Zed team and am following up from Dan Abramov's reply on Bluesky :)

I know very little about the Lean language or how y'alls dev tools fit together, how essential is the InfoView and LSP extensions to y'alls work with Lean?

This is true for proof assistants more broadly, but something analogous to the infoview is pretty essential since the editing process is interactive. As you construct a proof, the infoview keeps track of the current context and remaining obligations. The vscode version also has a bunch of other stuff like tooltips, warnings/errors, links, copy to clipboard, etc. that people would probably have a very hard time leaving behind now.

I'm somewhat surprised to hear this would be a big ask for zed since there are already all kinds of alternative panes that seem to be syncd to the editor state, like the assistant panel. I guess the machinery for that just isn't extensible. Assuming this has to do with Zed not secretly being a web browser?

[Marc Huisinga]

Mikayla Maki said:

I know very little about the Lean language or how y'alls dev tools fit together, how essential is the InfoView and LSP extensions to y'alls work with Lean? We'd need to make some big changes to support UI extensions and LSP extensions. Lean might be a good test case for us to keep in mind when we start that work, but unfortunately we have quite a bit queued up ahead of it. If there's a subset of tooling we could make available in Zed, we can make it happen :)

Some information on our use of LSP below.

Extensions

I'd say that having some kind of InfoView that can display proof goal states and expected types is essential when using Lean as a theorem prover, not just as a programming language. The easiest way to get a non-interactive variant of this is to implement support for the $/lean/plainGoal and $/lean/plainTermGoal requests, as well as some separate (potentially plain text) panel where this information can be displayed.

The other thing that I'd argue is essential is support for the $/lean/fileProgress notification that is used by the language server to report how far it has processed the file. Semantic analysis is very expensive in Lean, so files can take up to minutes to process entirely, so it must be obvious to users for which parts of the file they can expect language server features to work quickly. In VS Code, we display an orange bar in the file gutter for parts of the file that haven't been processed yet.

VS Code and NeoVim use $/lean/fileProgress, but they do not use $/lean/plainGoal and $/lean/plainTermGoal. Instead, they implement support for an RPC protocol that allows clients to call functions implemented in Lean directly. These are the $/lean/rpc/connect and $/lean/rpc/call requests, as well as the $/lean/rpc/release and $/lean/rpc/keepAlive notifications. This RPC protocol is then used by the client to obtain the goal state and the expected type, as well as to provide interactive features (e.g. recursive hovers or go-to-definition) for the information displayed in the InfoView as the user clicks or hovers on parts of the InfoView. It is possible to live without InfoView interactivity, but it is also very inconvenient.

Finally, through RPC, VS Code (but not NeoVim) supports widgets, which allow rendering interactive user interfaces from Lean code in the InfoView. This essentially requires that your InfoView is a web browser. Widgets are neat and helpful in some domains, but (currently) definitely not essential.

Some other smaller noteworthy extensions are the following:

• A fullRange field on diagnostics: The language server often truncates diagnostic ranges at the first line so that the editor isn't drenched in red squigglies, but it is sometimes still helpful to have the full range of the diagnostic available. For example, the VS Code and NeoVim InfoView implementations display the diagnostics at the current text cursor position as defined by the fullRange field, not the range field.
• A leanTags field on diagnostics: The Lean language server assigns some diagnostics a Lean-specific tag so that clients can distinguish them from other diagnostics, without rendering anything in the user interface (as e.g. diagnostic error codes often do). VS Code and NeoVim use these for goals accomplished and unsolved goals editor decorations.
• A dependencyBuildMode field on DidOpenTextDocumentParams: Clients can use this field to designate whether the Lean language server should automatically trigger a rebuild when opening a file. Since processing files is so expensive in Lean, the default in VS Code is that dependencies are not rebuilt automatically when the file is opened, only when users explicitly use a 'Restart File' command, and this field can be set to control this behavior. 'Restart File' is usually just implemented by closing and re-opening the file with dependencyBuildMode set to once, whereas files are initially opened with dependencyBuildMode set to never.

Protocol violations

The most significant of our LSP protocol violations is in the semantic highlighting and inlay hints requests: Since VS Code has no support for partial result reporting, but updating the semantic highlighting and the inlay hints of a file while it is still being processed is essential when this can take up to minutes, we simulate partial result reporting for these requests:
Instead of reporting the semantic tokens and inlay hints for the full file (as required by LSP), we only report the semantic tokens and the inlay hints for the parts of the file that have already been processed and then ask the client to emit another request by emitting the workspace/semanticTokens/refresh and workspace/inlayHint/refresh requests. This process continues until we have reported the full response for the full file. It requires that clients can deal with partial responses to semantic highlighting and inlay hint requests, that clients honor refresh requests and (for performance reasons) that they do not actually emit semantic highlighting and inlay hints requests for all open files in the workspace, only those that are visible. None of these things are required by LSP, but semantic highlighting and inlay hints would be unusable in Lean without it.

There are also other smaller protocol violations in our language server, e.g. due to the expensive nature of processing a file, we also require clients to emit textDocument/didOpen (which is not really required by LSP, but most clients do it regardless), or we currently don't really honor client capabilities at all yet and expect Lean clients to be mostly fully featured. I'm sure there are others that I don't even know about, too.

Full feature overview

The Lean 4 VS Code extension manual is the most complete resource for the set of features that is provided by the combination of the VS Code extension and the language server. Inlay hints and editor decorations are still missing from the manual at the moment, though.

[Marc Huisinga]

Perhaps also one final word of caution: Lean and its language server are still evolving quickly. Support for the Lean language server will require some gradual maintenance effort as the language and the language server evolve.