Create a Lean 4 project using leanpkg and open the project folder with VSCode. If you have a global installation of Lean 4, e.g. using elan default leanprover/lean4:nightly as described in the documentation above, you can also just open single .lean files independent of a project folder.
Open a .lean file and type in #eval 1. The extension should display a blue underline below #eval. Upon hovering over it, a hover panel reporting the result of the evaluation should pop up. When hovering over the 1, a hover panel displaying the type of 1 should pop up.
If no blue underline is displayed, make sure that Lean 4 is installed correctly by running lean --version in your project folder. The VSCode extension will not activate if it cannot find the lean command or lean --version reveals that Lean 3 is installed instead.
If the blue underline is displayed but the type is not displayed when hovering over 1, make sure that you are using a nightly build of Lean 4, not the stable version.
Create a Lean 4 Nix project and run the pinned version of VSCode as described here.
Refreshing file dependencies
As of now, after changing and rebuilding the dependency of a Lean 4 file, the language server needs to be manually informed that it should re-elaborate the full file, including the imports. This can be done using the Lean 4: Refresh File Dependencies command, which can be activated via Ctrl+Shift+X by default.
As of now, the extension supports the following features:
Syntax highlighting with basic Lean 4 syntax rules