unknown package 'Mathlib'

Stream: new members

[Yagub Aliyev]

I am trying to use VS for my project. What does it mean "unknown package 'Mathlib'"?
image.png

[Kevin Buzzard]

That does not look like a correctly-formatted lean repo, for example you're missing the json file whose name escapes me but which should definitely be there. Start again with lake new MyProject math, then lake exe cache get in the project repo, then open the project repo root directory with VS Code

[Yagub Aliyev]

Thank you for the hints. It works now.
image.png

[Kevin Buzzard]

Oh that was it -- lake-manifest.json. Not entirely sure what it does but it's definitely important :-)