Zulip Chat Archive

Stream: general

Topic: using lean via vscode


view this post on Zulip jeremy (Aug 18 2019 at 07:17):

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

view this post on Zulip Scott Morrison (Aug 18 2019 at 07:24):

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

view this post on Zulip Scott Morrison (Aug 18 2019 at 07:25):

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

view this post on Zulip Scott Morrison (Aug 18 2019 at 07:25):

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

view this post on Zulip Patrick Massot (Aug 18 2019 at 09:53):

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

view this post on Zulip Scott Morrison (Aug 18 2019 at 11:36):

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

view this post on Zulip Floris van Doorn (Aug 19 2019 at 13:28):

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


Last updated: May 06 2021 at 22:13 UTC