Lean's interface to VScode

Stream: new members

[Ching-Tsun Chou]

I'm curious about how Lean's interface to VScode works. Is there a paper or document on this subject?

[Henrik Böving]

It's an implementation of the LSP protocol (https://microsoft.github.io/language-server-protocol/) with a partially custom integration into VSCode for things like the infoview, though lots of stuff like e.g. auto complete is also standard LSP stuff. There is no publication about this, I also doubt this would really be publishable anywhere.

[David Thrane Christiansen]

The widgets system has a paper: https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2023.24

[Oliver Dressler]

As mentioned the main interactivity is provided via the LSP.

There are various extensions and violations to the protocol to provide additional features.
This comment (by @Marc Huisinga ) and the links it mentions are a great starting point:
https://leanprover.zulipchat.com/#narrow/channel/113488-general/topic/Lean.20.2B.20Zed.20integration/near/505671509

The source code for the VSCode extension is available here:
https://github.com/leanprover/vscode-lean4

Note that the extension is made up of several somewhat separate components. E.g. the Infoview ("lean4-infoview" in the repo) is its own React webapp because a custom panel in VSCode is just a webview.
You can look under the hood and inspect the webview using (Ctrl+Shift+P and "Open Webview Developer Tools).

If you want to know more details about the different LSP methods, I have attempted to document them while developing leanclient:
https://leanclient.readthedocs.io/en/latest/api.html

While the package might not be relevant, this documentation includes a short description, example response and links to the specification as well as the lean source code where it is implemented. The line numbers are definitely not up to date but the files should be mostly correct.