problem with leanpkg.toml

Stream: new members

[Eduardo Freire dos Santos]

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?

[Eduardo Freire dos Santos]

Here is the error image.png

[Jiekai]

After manually downloading the repo, what commands did you run?

[Eduardo Freire dos Santos]

I opened vscode and ran leanpkg configure

[Jiekai]

Is the _target directory there?

[Eduardo Freire dos Santos]

it is not

[Jiekai]

Do you have the leanpkg configure output?

[Eduardo Freire dos Santos]

Yes, it only
says " failed to open file 'leanpkg.toml' "

[Jiekai]

What does git status say?

[Eduardo Freire dos Santos]

fatal: not a git repository (or any of the parent directories): .git

[Jiekai]

How did you manually dowload the repo?

[Dudu]

Oh, not in the correct way apparently. I clicked on the code button in the github page (https://github.com/leanprover-community/tutorials) and dowloaded the zip file then extracted the tutorial-master folder to my thmProver directory.

[Dudu]

Ok, I ran git init and added all the files in the directory to the repository and committed it. Now git status says "On branch master
nothing to commit, working tree clean"

[Dudu]

But leanpkg configure still cannot open leanpkg.toml

[Dudu]

image.png

[Eric Wieser]

That certainly looks weird

[Scott Morrison]

Please start again following the instructions at https://leanprover-community.github.io/install/project.html

[Scott Morrison]

You should be using leanproject get tutorials.

[Jiekai]

Is the leanpkg source code in the lean repo?

@Dudu I think manually downloading mathlib and put the repo here

.
├── leanpkg.path
├── leanpkg.toml
├── LICENSE
├── mk_exercises.py
├── README.md
├── src
└── _target
    └── deps
        └── mathlib

Then run the following command would work.
Kevin Buzzard said:

Try lean -M6000 --make src if compiling lean crashes your laptop

[Jiekai]

I'm in China and I totally feel the network failure pain.

[Scott Morrison]

Please don't tell people to manually download things and put them places. It's a recipe for undiagnosable problems. Please use the tooling!