lean project

Stream: new members

[Yunlong LIN]

I am new in lean
image.png
I am not sure why this is not work when using leanproject. folder created by leanproject new ....

[Alex J. Best]

What was the output of leanproject new? Or if you try again what does it say

[Kevin Buzzard]

You don't have a _target directory in your project. Try leanproject get-mathlib-cache in the root directory of your repo.