Add lake to path

Stream: new members

[Vasily Ilin]

I followed the generic Linux installation instructions (single command): https://leanprover-community.github.io/install/linux.html. Lean works but lake is not in my path. E.g. lake update does not work. How do I add it to path?

[Patrick Massot]

Did you try opening a new terminal?

[Patrick Massot]

What shell are you using?

[Shreyas Srinivas]

Which Linux distro are you using?

[Shreyas Srinivas]

Patrick Massot : it sometimes happens that ~/.elan/bin is not added to the PATH. I had a recent experience like this which I have reported.

[Shreyas Srinivas]

I can't pinpoint the exact nature of the change, but somehow Ubuntu 24.04 seems more restrictive with permissions. I had to modify quite a few scripts in the past week to explicitly add write or execute permission. This wasn't the case with the 20.04 derived mint.

[Shreyas Srinivas]

I think it could be this thing: https://ubuntu.com/blog/whats-new-in-security-for-ubuntu-24-04-lts