Zulip Chat Archive

Stream: new members

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

Alexandre Rademaker (Sep 17 2020 at 01:25):

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 (Sep 17 2020 at 01:30):

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

Bryan Gin-ge Chen (Sep 17 2020 at 01:34):

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 (Sep 17 2020 at 03:03):

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

Last updated: Dec 20 2023 at 11:08 UTC