Zulip Chat Archive

Stream: new members

Topic: VS Code


view this post on Zulip Philip Vetter (Jul 13 2020 at 06:43):

You are running Lean in a directory without a leanpkg.toml file, this is NOT
supported. Please open the directory containing the leanpkg.toml file
instead (using "File / Open Folder..."). More details here

view this post on Zulip Shing Tak Lam (Jul 13 2020 at 06:47):

Did you open the src folder in VS Code? If so you want to go up a directory and open the folder which contains the src folder in VSCode

view this post on Zulip Philip Vetter (Jul 13 2020 at 06:51):

Please be more specific where this src folder would be located.

view this post on Zulip Shing Tak Lam (Jul 13 2020 at 06:52):

So I assume you opened a .lean file in VSCode?

Are you working in a Lean project or not?

view this post on Zulip Johan Commelin (Jul 13 2020 at 06:55):

@Philip Vetter Did you follow https://leanprover-community.github.io/install/project.html ?

view this post on Zulip Philip Vetter (Jul 13 2020 at 06:56):

I am following the directions in
https://leanprover-community.github.io/install/linux.html
I have downloaded elan-init.sh and executed it and it replied
stable installed - Lean (version 3.17.1, commit 05d7184a6642, Release)
I installed VS Code with leanprover . Step 5 fails. I have also installed emac lean extension.

view this post on Zulip Philip Vetter (Jul 13 2020 at 06:58):

No I am following https://leanprover-community.github.io/install/linux.html
is that wrong?

Johan Commelin said:

Philip Vetter Did you follow https://leanprover-community.github.io/install/project.html ?

view this post on Zulip Johan Commelin (Jul 13 2020 at 06:59):

No, I thought you were already a bit further. That page should be fine.

view this post on Zulip Scott Morrison (Jul 13 2020 at 06:59):

@Philip Vetter, there are two steps --- first an OS-specific installation step, for which you are correctly using https://leanprover-community.github.io/install/linux.html, and second a step to set up a project, following https://leanprover-community.github.io/install/project.html

view this post on Zulip Johan Commelin (Jul 13 2020 at 07:00):

If you want, you can share your screen via Zoom, and we can try to fix it.

view this post on Zulip Scott Morrison (Jul 13 2020 at 07:00):

If you're trying to verify Step 5 from https://leanprover-community.github.io/install/linux.html, could you say exactly what fails?

view this post on Zulip Philip Vetter (Jul 13 2020 at 07:03):

Ah I see. Instructions said something about click reload. (where is that?)
I restarted VSC and it works!

view this post on Zulip Scott Morrison (Jul 13 2020 at 07:04):

Now see if https://leanprover-community.github.io/install/project.html works!

view this post on Zulip Philip Vetter (Jul 13 2020 at 09:17):

In VSCode, when viewing the tutorial exercises are partially covered by a column of preview images of the text. Is this normal and how can I move it?

view this post on Zulip Johan Commelin (Jul 13 2020 at 09:18):

I don't understand what you mean. Could you paste a screenshot?

view this post on Zulip Markus Himmel (Jul 13 2020 at 09:19):

Do you mean the minimap? You can disable it by selecting "View > Show Minimap"

view this post on Zulip Philip Vetter (Jul 13 2020 at 09:23):

Yes this works. Is it possible to move it off of the text? I could not hear someone's comments.

view this post on Zulip Scott Morrison (Jul 13 2020 at 09:23):

No. Just turn it off, it's not helpful.

view this post on Zulip Philip Vetter (Jul 13 2020 at 09:24):

ok thank you!

view this post on Zulip Patrick Massot (Jul 13 2020 at 09:25):

You should watch https://www.youtube.com/watch?v=CM0wYOrYII8&list=PLlF-CfQhukNnxF1S22cNGKyfOrd380NUv&index=6&t=0s this is covered there


Last updated: May 08 2021 at 05:14 UTC