How to setup lean4 vscode extension

Stream: lean4

[Lim, Thing-han]

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

[Lim, Thing-han]

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

[Marc Huisinga]

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]

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

[Marc Huisinga]

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]

Perhaps I should mention that in the README :)

[Lim, Thing-han]

I installed lean4 0.0.7 from the extension tab

[Marc Huisinga]

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]

ah I got it, I installed the release version.

[Lim, Thing-han]

So that's why it doesn't work!

[Lim, Thing-han]

Thank you!

[Marc Huisinga]

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

[Lim, Thing-han]

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]

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

[Lim, Thing-han]

Yes

[Marc Huisinga]

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]

Got it ! Thank you!!