Zulip Chat Archive

Stream: lean4

Topic: How to setup lean4 vscode extension


view this post on Zulip 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....

view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip 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...

view this post on Zulip 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.

view this post on Zulip Marc Huisinga (Feb 24 2021 at 15:06):

Perhaps I should mention that in the README :)

view this post on Zulip Lim, Thing-han (Feb 24 2021 at 15:06):

I installed lean4 0.0.7 from the extension tab

view this post on Zulip 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

view this post on Zulip Lim, Thing-han (Feb 24 2021 at 15:08):

ah I got it, I installed the release version.

view this post on Zulip Lim, Thing-han (Feb 24 2021 at 15:08):

So that's why it doesn't work!

view this post on Zulip Lim, Thing-han (Feb 24 2021 at 15:08):

Thank you!

view this post on Zulip Marc Huisinga (Feb 24 2021 at 15:09):

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

view this post on Zulip 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

view this post on Zulip Marc Huisinga (Feb 24 2021 at 15:17):

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

view this post on Zulip Lim, Thing-han (Feb 24 2021 at 15:18):

Yes

view this post on Zulip 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.

view this post on Zulip Lim, Thing-han (Feb 24 2021 at 15:21):

Got it ! Thank you!!


Last updated: May 07 2021 at 13:21 UTC