## Stream: lean4

### Topic: How to setup lean4 vscode extension

#### Lim, Thing-han (Feb 24 2021 at 14:31):

I installed from marketplace at first, it didn't work then, and somehow it works now....

#### Lim, Thing-han (Feb 24 2021 at 14:41):

By the way, how can I go to definition or view type by hover over the term?

#### Marc Huisinga (Feb 24 2021 at 14:54):

If e.g. #eval 1 displays a blue underline with the evaluated term, it should work out of the box. Hovering over names should show their types and you should be able to go to definition either with RMB > Go to definition or F12.

#### Lim, Thing-han (Feb 24 2021 at 15:01):

eval do works, however neither hovering over names nor go to definition by pressing F12 work for me...

#### Marc Huisinga (Feb 24 2021 at 15:05):

Which version of Lean 4 did you install? Hovering and go to definition do not work with the old "release" version of lean4, only the nightly builds.

#### Marc Huisinga (Feb 24 2021 at 15:06):

Perhaps I should mention that in the README :)

#### Lim, Thing-han (Feb 24 2021 at 15:06):

I installed lean4 0.0.7 from the extension tab

#### Marc Huisinga (Feb 24 2021 at 15:07):

That's the VSCode extension, but one also needs to install Lean 4 itself, as described here: https://leanprover.github.io/lean4/doc/setup.html

#### Lim, Thing-han (Feb 24 2021 at 15:08):

ah I got it, I installed the release version.

#### Lim, Thing-han (Feb 24 2021 at 15:08):

So that's why it doesn't work!

Thank you!

#### Marc Huisinga (Feb 24 2021 at 15:09):

No problem, I'll add it to the README so this is more obvious!

#### Lim, Thing-han (Feb 24 2021 at 15:13):

By the way, although not related, is there any command for compiling a project so that I can print some string to the command line for example

#### Marc Huisinga (Feb 24 2021 at 15:17):

Does leanpkg build as in https://leanprover.github.io/lean4/doc/setup.html#leanpkg work?

Yes

#### Marc Huisinga (Feb 24 2021 at 15:19):

Ah, the extension itself does not support any such command yet, most people seem to just use #eval for their REPL needs.

#### Lim, Thing-han (Feb 24 2021 at 15:21):

Got it ! Thank you!!

Last updated: May 07 2021 at 13:21 UTC