Lean 4 - VS Code extension parity #5059
Description
Check for existing issues
- Completed
Misc notes
Hello! I noticed that resolving the feature gap would likely require changes to the internals of Zed so I figured opening a tracking issue would be a good first step.
Context
Support for Lean 4 was introduced in PR #2482. The extension uses the official language server and tree-sitter-lean.
Although the extension is well-maintained, one of the remaining todo items is the InfoView (documented here) which is more or less required. Issue #1406 tracking the initial support for Lean 4 had a comment that referenced a discussion on the Lean community's Zulip chat.
From a cursory skim through the comments it looks like strict adherence to the language server protocol makes it impossible to implement such functionality. Apparently, both VS Code and Neovim allow for working around the spec while Zed currently does not.
Coordination
I'm not sure what the next steps here are nor who can detail the current limitations based on the technical summary from the aforementioned discussion. The following is a list of folks who were previously involved in such discussions; feel free to unsubscribe if no longer interested!
- @mikayla-maki Zed core developer
- @mhuisi member of Lean
- @owlx56 maintainer of the extension
- @Julian maintainer of tree-sitter-lean and lean.nvim
- @gaearon fellow would-be user
Additional Notes
I ended up here while updating our developer environments to reflect, in part, the increasing interest of our engineers in both Zed and formal verification.