Zulip Chat Archive

Stream: new members

Topic: problem with leanpkg.toml


Eduardo Freire dos Santos (Jul 17 2021 at 17:53):

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 (Jul 17 2021 at 17:54):

Here is the error image.png

Jiekai (Jul 17 2021 at 17:57):

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

Eduardo Freire dos Santos (Jul 17 2021 at 18:03):

I opened vscode and ran leanpkg configure

Jiekai (Jul 17 2021 at 18:05):

Is the _target directory there?

Eduardo Freire dos Santos (Jul 17 2021 at 18:06):

it is not

Jiekai (Jul 17 2021 at 18:07):

Do you have the leanpkg configure output?

Eduardo Freire dos Santos (Jul 17 2021 at 18:07):

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

Jiekai (Jul 17 2021 at 18:08):

What does git status say?

Eduardo Freire dos Santos (Jul 17 2021 at 18:08):

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

Jiekai (Jul 17 2021 at 18:11):

How did you manually dowload the repo?

Dudu (Jul 17 2021 at 18:14):

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 (Jul 17 2021 at 18:22):

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 (Jul 17 2021 at 18:23):

But leanpkg configure still cannot open leanpkg.toml

Dudu (Jul 17 2021 at 18:26):

image.png

Eric Wieser (Jul 17 2021 at 19:38):

That certainly looks weird

Scott Morrison (Jul 18 2021 at 05:08):

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

Scott Morrison (Jul 18 2021 at 05:08):

You should be using leanproject get tutorials.

Jiekai (Jul 18 2021 at 06:03):

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 (Jul 18 2021 at 06:04):

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

Scott Morrison (Jul 18 2021 at 06:18):

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


Last updated: Dec 20 2023 at 11:08 UTC