Mathlib + VScode

Stream: new members

[Strahinja Strahinja]

Hey everyone! Im trying to get lean to work with VSCode. I have followed the instructions step by step and I managed to successfully make a lean project and install the extension (It works perfectly fine for single file, tested). I have also installed the mathlib via pip3 and intagrated it into the project. However it still won't see it. On top of that it won't see any import files no matter where they are! THe only way it works is if I give it a realative path e.g: import ._target.deps.mathlib.src.topology.basic but then it breaks since I have to do so for EVERY import in every .lean file in mathlib. Also aplies for two files in projects src folder. If I have A.lean and B.lean and want to import A.lean into B.lean I have to type:
import .A instead of just A.
Can someone help me please. Here are some files I think are relevant. Thank you in advance!
image.png

[Eric Wieser]

You've opened the wrong folder, you need to open "test/project" not "test"

[Eric Wieser]

Your terminal output isn't relevant, because you're running everything in test/project (which gives the correct output), but vscode is running everything in the workspace root, test (which doesn't)