lake update gives error: error: [root]: no configuration file with a supported extension:

[ouboub]

Hi
I am on Ubuntu 24.04 (either with tcsh or bash shell)
I followed the instructions found in
https://leanprover-community.github.io/install/debian.html
and
https://leanprover-community.github.io/install/project.html
However, while the part

Go to a folder where you want to create a project in a subfolder my_project, and type lake +leanprover/lean4:nightly-2024-04-24 new my_project math. 

went smoothly, the next one

lake update

gave me the error

error: [root]: no configuration file with a supported extension:
././lakefile.lean
././lakefile.toml

I did run source ~/.profile
What do I miss?
Regards
Uwe Brauer

[digama0]

Perhaps you forgot to cd my_project after the lake new step? You should run lake commands in the folder that contains a lakefile.lean or lakefile.toml file, this is what marks the root of the project from lake's perspective.

[ouboub]

Perhaps you forgot to cd my_project after the lake new step? You should run lake commands in the folder that contains a lakefile.lean or lakefile.toml file, this is what marks the root of the project from lake's perspective.

Aah, sigh, I was in

~/ALLES/HGs/UserXXX/Pub/Preprints/Lean/mathematics_in_lean/my_project

Where I used the lake new step, it did not occur to me that there was another my_project subdirectory 😳

After so the correct directory where lake new should be used is

~/ALLES/HGs/UserXXX/Pub/Preprints/Lean/mathematics_in_lean/my_project/my_project

now everything works!

thanks

[ouboub]

well one comment I still have to make
du -h
tells me that

~/ALLES/HGs/Karp/Pub/Preprints/Lean/mathematics_in_lean

contains now 10 GB
basically the last lake new downloaded another 4 GB
isn't that a bit excessive?

[digama0]

Every lean project gets its own separate copy of mathlib and its build artifacts. Feel free to complain about this design on https://leanprover.zulipchat.com/#narrow/stream/270676-lean4 . (Note, I don't recommend having a lean project as a subdirectory of another one - I would move Lean/mathematics_in_lean/my_project/my_project to just Lean/my_project here. Yes it's safe to move lean project folders around on the file system.)