Having some issues with importing

Stream: new members

[Ryan Gold]

Every time I try to import something, an error appears in VS code, along the lines of
file 'data/nat/gcd' 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 primes.lean:1:0 invalid import: data.nat.gcd could not resolve import: data.nat.gcd
I tried reinstalling mathlib, and configured the project using the commands in the tutorial. Any help would be appreciated. (Using lean 3, by the way)

[Bryan Gin-ge Chen]

Which tutorial did you follow?

[Kevin Buzzard]

Did you look at the URL in the error message for the list of common reasons as to why this is happening?

[Ryan Gold]

I followed the instructions here: https://leanprover-community.github.io/install/project.html ,
I checked the URL, and it said it couldn't find a leanpkg.toml

[Kevin Buzzard]

I mean did you read the suggestions at https://leanprover-community.github.io/file-not-found.html

[Ryan Gold]

Yes, I did. I already completed the first of the two, and the second told me to enter leanproject get-mathlib-cache into the terminal, which I did.

This output Could not find a leanpkg.toml

[Bryan Gin-ge Chen]

How did you create your Lean project? Did you use something like leanproject new your_project_name?

[Kevin Buzzard]

If you haven't got a leanpkg.toml then you haven't got a valid lean project. Can you post a screenshot of VS Code showing the problem?

[Bryan Gin-ge Chen]

(Specifically, I think we'd like to see the files in the directory you've opened in VS Code.)

[Ryan Gold]

Think I got it fixed now. I screwed up something when configuring the directories.