Keep `lake` on the PATH in a GitHub codespace

Stream: general

[Vasily Ilin]

I am using a GitHub codespace, and I need lake to be on the PATH. I am able to get it with the command here but when I close the codespace and open it again, Lean is still installed but lake is not longer on the PATH. I don't know if it's an issue with the codespace or lake itself (I don't understand either one well enough, unfortunately). Can anyone explain how to keep lake on the path?

[Eric Wieser]

How did you create your codespace?

[Vasily Ilin]

I clicked on the big green button on Github that says "create codespace on master"
image.png

[Vasily Ilin]

I think the issue is that the global PATH is never updated or never saved. When I make a new terminal in the same codespace, lake is not on the PATH.
In this case I just need to know where the lake executable is and add to to the PATH. Where does the lake executable live?

[Eric Wieser]

That button does different things on different repos

[Vasily Ilin]

I see. It's this repo: https://github.com/Vilin97/autoformalization-with-llms