Zulip Chat Archive

Stream: new members

Topic: Mathlib + VScode


Strahinja Strahinja (Aug 21 2022 at 01:19):

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 (Aug 21 2022 at 11:15):

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

Eric Wieser (Aug 21 2022 at 11:16):

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)


Last updated: Dec 20 2023 at 11:08 UTC