file 'topology/basic' not found in the search path

Stream: new members

[Alexandre Rademaker]

I follow the steps from https://leanprover-community.github.io/install/project.html, I opened the VS Code and I am getting this error, any idea?

[Alexandre Rademaker]

OK, this is strange... It is working with Emacs...

[Bryan Gin-ge Chen]

You opened the entire my_project/ directory in VS Code, right? If you try to open just a standalone file the extension won't be able to find mathlib.

[Alexandre Rademaker]

Thank you, now it is clear that I need to open the complete directory not only the file.