Lean 4 VSCode Extension
This extension provides VSCode editor support for the Lean 4 programming language.
It is based upon the lsp-sample and includes code from vscode-lean.
Functionality
This extension is intended mostly for debugging purposes and to provide a tool to demonstrate Lean 4 with to users that are used to using Lean 3 together with VSCode. It is also supposed to provide an easily dissectible and minimal base for the Lean 3 community to work with and extend upon to port all the existing Lean 3 client features to Lean 4.
As of now, the extension supports the following features:
- Diagnostics
- Syntax highlighting with basic Lean 4 syntax rules
\foo
unicode shortcuts
- Command to refresh file dependencies using Ctrl+Shift+R after recompilation
- Type information & documentation on hover since leanprover/lean4@d7c201a2
- Breadcrumbs
Running the client
Add lean
to your PATH
(e.g. using elan
) and set your LEAN_PATH
if you are working on a project other than Lean 4 itself as described here. Then, install the extension from the marketplace. If you are using the nix setup, you can also run VSCode using the nix integration mentioned here.
You may first need to disable the Lean 3 VSCode extension if you have it installed.
Building the client
Assuming lean
is in your PATH
(e.g. using elan
):
- Run
npm install
in this folder. This installs all necessary npm modules.
- Open VS Code on this folder.
- Press Ctrl+Shift+B to compile the client.
- Switch to the Debug viewlet (Ctrl+Shift+D).
- Select
Launch Client
from the drop down.
- Run the launch config.
Code by vscode-lean
src/input.ts
, syntaxes
, language-configuration.json
, translations.json
and the code to load src/input.ts
in extension.ts
have been taken from vscode-lean.