Zulip Chat Archive

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
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.

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

Dan Velleman (Oct 28 2021 at 13:47):

I recently installed Lean on a Macintosh, and I'm using it with VS Code. Everything seems to be working, except that anytime I give a command that begins with #, VS Code reports that there is a problem. It doesn't say what the nature of the problem is. All it says is "no quick fixes available." The output of the command shows up correctly in the Lean infoview pane, so I could just ignore the problem reports. But it seems like something in VS Code isn't configured right. Any ideas? Has anyone else seen this?

Alex J. Best (Oct 28 2021 at 14:16):

Lean 3 or Lean 4?

Dan Velleman (Oct 28 2021 at 14:57):

Lean 3. Well, I thought I might want to use Lean 4, so I installed both, but I quickly realized that for the moment I should stick to Lean 3, so that's what I'm using.

Dan Velleman (Oct 28 2021 at 14:59):

I have both the lean and lean4 extensions installed in VS Code. Is that my problem? Should I remove lean4?

Kevin Buzzard (Oct 28 2021 at 15:01):

I have both installed and I don't see this problem

Alex J. Best (Oct 28 2021 at 15:02):

I find having both extensions enabled in the same workspace has causes me issues in the past, so I always disable either one or the other for any given workspace.

Kevin Buzzard (Oct 28 2021 at 15:03):

randomly searching this Zulip for your error -- did you use "open folder" to open a project folder rather than "open file"? Maybe you can just send a screenshot of your VS Code set-up with the explorer tab open on the left and the error visible?

Dan Velleman (Oct 28 2021 at 15:29):

Yes, I used "open folder". I'll take a screenshot.

Dan Velleman (Oct 28 2021 at 15:36):

Screen-Shot-2021-10-28-at-11.33.38-AM.png

Dan Velleman (Oct 28 2021 at 15:36):

In the screenshot, I have my mouse hovering over the #check command. That's what brings up the "problem" message. There is also a list of problems at the bottom of the window.

Kevin Buzzard (Oct 28 2021 at 15:39):

oh! I think this is just normal. I think these are not "problems" at all, just "output" which is being interpreted as "problems" by something. I just tried this on my VS Code and it does the same. I don't use the # commands much.

Kevin Buzzard (Oct 28 2021 at 15:39):

In code like mathlib there would be no # commands used at all, this is just for experimentation, trying to work out what types things have etc.

Dan Velleman (Oct 28 2021 at 15:40):

OK, I'll just ignore it. Thanks.

Ocschwar (Nov 07 2021 at 04:14):

Hi, I just installed VS Code and the Lean extension, and tried the tutorial exercises, but on VS code the prover is unable to find Mathlib. (from the terminal, running lean on the example files works fine). what do I do to get it to find those files?

Scott Morrison (Nov 07 2021 at 04:49):

Are you opening the folder in VSCode (the folder containing leanpkg.toml, in particular)? Opening individual files won't work.

Scott Morrison (Nov 07 2021 at 04:49):

If so, please show us which file you are opening, and exactly what the error message is.

Ocschwar (Nov 07 2021 at 05:01):

00_first_proofs.lean:1:0
Messages (2)
00_first_proofs.lean:1:0
file 'data/real/basic' not found in the search path
Use 'lean --path' to see where lean is looking, or https://leanprover-community.github.io/file-not-found.html for more

Scott Morrison (Nov 07 2021 at 05:29):

Scott Morrison said:

Are you opening the folder in VSCode (the folder containing leanpkg.toml, in particular)? Opening individual files won't work.

Could you answer this?

Scott Morrison (Nov 07 2021 at 05:49):

Alternatively a screen-shot of your VScode window could help.

Kevin Buzzard (Nov 07 2021 at 10:12):

Did you read the web page mentioned in the error? Your situation can be caused by a number of errors in your set-up and some are listed there.

Kevin Buzzard (Nov 07 2021 at 10:12):

And did you install the community tools following the instructions on the community website?

Ocschwar (Nov 07 2021 at 19:55):

If you mean this https://leanprover-community.github.io/install/macos.html , yes.

Ocschwar (Nov 07 2021 at 19:56):

I ran the curl command, installed everything, and started VSCode.

Ocschwar (Nov 07 2021 at 19:57):

"Are you opening the folder in VSCode (the folder containing leanpkg.toml, in particular)? Opening individual files won't work."

Yes. Opening the folder.

Kevin Buzzard (Nov 07 2021 at 21:15):

Send a screenshot of the full VS Code window. If it's working in the terminal then it should work in VS Code. Have the file explorer open on the left.

Ocschwar (Nov 08 2021 at 00:55):

Screen-Shot-2021-11-07-at-7.55.33-PM.png

Kevin Buzzard (Nov 08 2021 at 00:56):

you have not opened the root folder of the project you're working on in VS Code

Kevin Buzzard (Nov 08 2021 at 00:56):

you have opened some other folder above it

Kevin Buzzard (Nov 08 2021 at 00:57):

you need to open the folder containing the file leanpkg.path for the project (in your case a folder called tutorials) using VS Code's "open folder" functionality; that is how VS Code will figure out the paths to all the imports. This is what Scott was saying earlier.

Ocschwar (Nov 08 2021 at 02:44):

Just checked, and yes, that's precisely the issue. Thanks so much!

Last updated: Dec 20 2023 at 11:08 UTC

Stream: new members

Topic: VS Code

Philip Vetter (Jul 13 2020 at 06:43):

Shing Tak Lam (Jul 13 2020 at 06:47):

Philip Vetter (Jul 13 2020 at 06:51):

Shing Tak Lam (Jul 13 2020 at 06:52):

Johan Commelin (Jul 13 2020 at 06:55):

Philip Vetter (Jul 13 2020 at 06:56):

Philip Vetter (Jul 13 2020 at 06:58):

Johan Commelin (Jul 13 2020 at 06:59):

Scott Morrison (Jul 13 2020 at 06:59):

Johan Commelin (Jul 13 2020 at 07:00):

Scott Morrison (Jul 13 2020 at 07:00):

Philip Vetter (Jul 13 2020 at 07:03):

Scott Morrison (Jul 13 2020 at 07:04):

Philip Vetter (Jul 13 2020 at 09:17):

Johan Commelin (Jul 13 2020 at 09:18):

Markus Himmel (Jul 13 2020 at 09:19):

Philip Vetter (Jul 13 2020 at 09:23):

Scott Morrison (Jul 13 2020 at 09:23):

Philip Vetter (Jul 13 2020 at 09:24):

Patrick Massot (Jul 13 2020 at 09:25):

Dan Velleman (Oct 28 2021 at 13:47):

Alex J. Best (Oct 28 2021 at 14:16):

Dan Velleman (Oct 28 2021 at 14:57):

Dan Velleman (Oct 28 2021 at 14:59):

Kevin Buzzard (Oct 28 2021 at 15:01):

Alex J. Best (Oct 28 2021 at 15:02):

Kevin Buzzard (Oct 28 2021 at 15:03):

Dan Velleman (Oct 28 2021 at 15:29):

Dan Velleman (Oct 28 2021 at 15:36):

Dan Velleman (Oct 28 2021 at 15:36):

Kevin Buzzard (Oct 28 2021 at 15:39):

Kevin Buzzard (Oct 28 2021 at 15:39):

Dan Velleman (Oct 28 2021 at 15:40):

Ocschwar (Nov 07 2021 at 04:14):

Scott Morrison (Nov 07 2021 at 04:49):

Scott Morrison (Nov 07 2021 at 04:49):

Ocschwar (Nov 07 2021 at 05:01):

Scott Morrison (Nov 07 2021 at 05:29):

Scott Morrison (Nov 07 2021 at 05:49):

Kevin Buzzard (Nov 07 2021 at 10:12):

Kevin Buzzard (Nov 07 2021 at 10:12):

Ocschwar (Nov 07 2021 at 19:55):

Ocschwar (Nov 07 2021 at 19:56):

Ocschwar (Nov 07 2021 at 19:57):

Kevin Buzzard (Nov 07 2021 at 21:15):

Ocschwar (Nov 08 2021 at 00:55):

Kevin Buzzard (Nov 08 2021 at 00:56):

Kevin Buzzard (Nov 08 2021 at 00:56):

Kevin Buzzard (Nov 08 2021 at 00:57):

Ocschwar (Nov 08 2021 at 02:44):