Zulip Chat Archive

Stream: new members

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


view this post on Zulip 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?

view this post on Zulip Alexandre Rademaker (Sep 17 2020 at 01:30):

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

view this post on Zulip 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.

view this post on Zulip 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: May 14 2021 at 04:22 UTC