problem with leanpkg.toml

Stream: general

[单丹]

Hello, I am following the "Work on an existing project" section on the Lean projects page (https://leanprover-community.github.io/install/project.html) and keep getting this error. I've tried manually dowloading the repository from github, but I still get problems with the leankpg.toml file, namely git bash says that it cannot open it. Any suggestions on how to fix this?

[单丹]

issue.png

[Kevin Buzzard]

That doesn't look like the right command to me. Where are you seeing the suggestion to type leanpkg? Mathlib is in the leanprover-community GitHub account and the commands you're typing don't mention this. Why aren't you using leanproject new to make your project?

[单丹]

I saw it in a blog tutorial about lean. I followed the steps in https://leanprover-community.github.io/leanproject.html to use leanproject, and got the same problem

[单丹]

issue-2.png

[Reid Barton]

I think you want to do a cd my_project after leanpkg new.

[ZeHe]

Sorry, I don't quite understand what you mean. My English is not very good. I firstly used leanproject get tutorials, and then I create a new lean file at the exercise file. It works well. But after I restart vscode, it fails again. After that I delete the tutorials file and then download it agian, the error failed to open file 'leanpkg. toml' appears all the time

[Reid Barton]

leanproject new my_project creates a new project that will be in the directory /c/C++_exp/lean/my_project. But after running leanproject new my_project, you are still in the original directory /c/C++_exp/lean, as your shell prompt shows.

[Reid Barton]

If you want to run commands that apply to your new project (like leanproject build) then you need to change directories by typing cd my_project first.

[ZeHe]

It doesn't seem to work?or just i‘m so stupid…… issue1.png

[Alex J. Best]

You need to use the "File: open folder" option in the main menu of VSCode to open the folder "my_project" rather than the folder "Lean"

[ZeHe]

Thank you for your help, now it's early morning here, I have to rest because there is an exam in the morning, I will continue to try to solve the problem later

[ZeHe]

(deleted)

[ZeHe]

Alex J. Best said:

You need to use the "File: open folder" option in the main menu of VSCode to open the folder "my_project" rather than the folder "Lean"

Thank you guys, I have solved the problem and can use it normally.What you said is exactly the problem.