program not found

Stream: lean4

[Ashvni Narayanan]

Hello. I have Lean 4 installed and have been using mathlib4 for a while. This morning, I tried to update it using the instructions given here : https://github.com/leanprover-community/mathlib4/wiki/Using-mathlib4-as-a-dependency
After lake update ran, I got an error that the server had crashed thrice in the last minute, so it would not restart. As a result, lake update terminated unsuccessfully. After this, the server has not restarted. I keep getting the following errors when I try to restart :

error: command failed: 'lean'
info: caused by: program not found
[Error - 9:34:40 AM] The Lean 4 server crashed 1 times in the last 3 minutes. The server will not be restarted. See the output for more information.
[Error - 9:34:40 AM] Server initialization failed.
  Message: Pending response rejected since connection got disposed
  Code: -32097
[Error - 9:34:40 AM] Lean 4 client: couldn't create connection to server.
  Message: Pending response rejected since connection got disposed
  Code: -32097

Any help is appreciated, thank you!

[Scott Morrison]

You say "using mathlib4", but then linked to the instructions for "using mathlib4 as a dependency". Running lake update inside the mathlib4 directory itself is not advised. (except for maintainers who are intentionally bumping upstream projects)

[Scott Morrison]

Could this be the source of your problem?

[Ashvni Narayanan]

Apologies for the confusion, I want to use mathlib4 as a dependency in a project. I am now following the instructions given here under Creating a Lean project : https://leanprover-community.github.io/install/project.html
When I try the second step (applying lake update), I get the following error:
C:/Users/ashvn/.elan/bin/lake.exe: error while loading shared libraries: ?: cannot open shared object file: No such file or directory
I am not sure what is wrong.

[Mac Malone]

@Ashvni Narayanan How did you install Lean?

[Ashvni Narayanan]

Hi @Mac Malone , I had installed it a long time ago using the instructions on the page.
Ultimately, I decided to uninstall and reinstall elan. I also deleted an lake-toolchain file, which I believe was causing the error. I then followed instructions to create a new project dependent on mathlib4. It is now finally working!