using lean via vscode

Stream: general

[jeremy]

Hi,

On the web page https://leanprover.github.io/reference/using_lean.html it says
says 1.2. Using Lean with VSCode
Assuming you have installed Lean and Visual Studio Code, you can add the
Lean extension to VSCode by clicking the extension icon in the view bar
at left and searching for lean. Once you have installed the extension,
clicking on lean in the extensions panel provides additional information.

What is this extension icon?

On another web page which I was directed to , namely
https://github.com/leanprover-community/mathlib/blob/master/docs/install/linux.md
it says
Click on the extension icon (image of icon) in the side bar on the left edge of the screen and search for leanprover
but there isn't any icon on the vscode window which looks like the image in the instructions

[Scott Morrison]

Oh dear, they've updated all the icons in VS Code...

[Scott Morrison]

It now looks like 3 squares in an L shape, with a 4th square on the top right. Hovering over it should say "extensions".

[Scott Morrison]

If you're using mac, it's shift-cmd-X to open the extensions tab.

[Patrick Massot]

All this clicking is awfully hard to document. The easy way is: open a terminal and type code --install-extension jroesch.lean

[Scott Morrison]

Except that on a mac (and I don't know about windows), there won't be code available on the command line... :-(

[Floris van Doorn]

On Windows you can open the extensions tab with ctrl+shift+X