Zulip Chat Archive

Stream: general

Topic: problem with leanpkg.toml

单丹 (Nov 09 2022 at 15:46):

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?

单丹 (Nov 09 2022 at 15:47):


Kevin Buzzard (Nov 09 2022 at 15:50):

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?

单丹 (Nov 09 2022 at 15:55):

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

单丹 (Nov 09 2022 at 15:56):


Reid Barton (Nov 09 2022 at 15:57):

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

ZeHe (Nov 09 2022 at 16:06):

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 (Nov 09 2022 at 16:15):

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 (Nov 09 2022 at 16:15):

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 (Nov 09 2022 at 16:41):

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

Alex J. Best (Nov 09 2022 at 16:43):

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 (Nov 09 2022 at 16:50):

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 (Nov 10 2022 at 04:17):


ZeHe (Nov 10 2022 at 04:18):

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.

Last updated: Aug 03 2023 at 10:10 UTC