Stream: new members
Topic: VS Code
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
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
Philip Vetter (Jul 13 2020 at 06:51):
Please be more specific where this src folder would be located.
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?
Johan Commelin (Jul 13 2020 at 06:55):
@Philip Vetter Did you follow https://leanprover-community.github.io/install/project.html ?
Philip Vetter (Jul 13 2020 at 06:56):
I am following the directions in
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.
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 ?
Johan Commelin (Jul 13 2020 at 06:59):
No, I thought you were already a bit further. That page should be fine.
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
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.
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?
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!
Scott Morrison (Jul 13 2020 at 07:04):
Now see if https://leanprover-community.github.io/install/project.html works!
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?
Johan Commelin (Jul 13 2020 at 09:18):
I don't understand what you mean. Could you paste a screenshot?
Markus Himmel (Jul 13 2020 at 09:19):
Do you mean the minimap? You can disable it by selecting "View > Show Minimap"
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.
Scott Morrison (Jul 13 2020 at 09:23):
No. Just turn it off, it's not helpful.
Philip Vetter (Jul 13 2020 at 09:24):
ok thank you!
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