permission denied error code: 13

Stream: new members

[Byung-Hak Hwang]

Hello,

I’m encountering a permission error and haven’t been able to resolve it.
A couple of days ago, I had no issues building and running lake and lean.
However, after deleting my local repository and re-cloning the project from the global repository,
both lake build and lake exe get cache started showing permission errors.

I can temporarily resolve the issue by granting permissions in the terminal using commands like sudo lake build,
but the same issue persists when working in VS Code.

How can I permanently fix this issue?

stderr:
info: mathlib: URL has changed; deleting '././.lake/packages/mathlib' and cloning again
error: permission denied (error code: 13)
  file: ././.lake/packages/mathlib/CODE_OF_CONDUCT.md
Invalid Lake configuration.  Please restart the server after fixing the Lake configuration file.

[Henrik Böving]

What are the file permissions on that file? ls -la .lake/build/packages/mathlib/CODE_OF_CONDUCT.md

[Byung-Hak Hwang]

Henrik Böving 말함:

What are the file permissions on that file? ls -la .lake/build/packages/mathlib/CODE_OF_CONDUCT.md

I got -rw-r--r--  1 root  staff  5319 11 30 01:04 CODE_OF_CONDUCT.md

[Kevin Buzzard]

So it can't be deleted because it's owned by root. Did you clone the project when logged in as root or something? How about just deleting everything and cloning again as the user who wants to use the repo? sudo lake build won't solve the problem, you're just using the repo as root so it will just cause more problems (it will create a bunch more files which will then also be owned by root and hence undeletable by you unless you use sudo yet again). You'd be better off doing sudo rm -rf .lake. Are the regular lean files also owned by root? Just delete everything and start again and don't use sudo at all, is my advice.

[Byung-Hak Hwang]

Kevin Buzzard 말함:

So it can't be deleted because it's owned by root. Did you clone the project when logged in as root or something? How about just deleting everything and cloning again as the user who wants to use the repo? sudo lake build won't solve the problem, you're just using the repo as root so it will just cause more problems (it will create a bunch more files which will then also be owned by root and hence undeletable by you unless you use sudo yet again). You'd be better off doing sudo rm -rf .lake. Are the regular lean files also owned by root? Just delete everything and start again and don't use sudo at all, is my advice.

Thank you for the advice. Following your suggestion, I entirely deleted, set the right permissions, and cloned it again, and now it works!

[Andrei Burdușa]

Thank you! This was very helpful! I also had to remove .elan from the home directory, but eventually was able to use lake again.