Lean 4 online version installation

Stream: general

[Mohamamd Awheeo]

I am trying to run the lean server but it shows that lake is not installed. How to install Lake:
image.png

[Jon Eugster]

If you are new to Lean and never installed elan (i.e. if which elan prints nothing), you should probably look at How To Get Started with Lean.

[Jon Eugster]

(PS if you do have Lean installed, i.e. all of which lean elan lake are found on your system, and you still have troubles with lean4web, please DM me :smile: )

[Mohamamd Awheeo]

Jon Eugster said:

(PS if you do have Lean installed, i.e. all of which lean elan lake are found on your system, and you still have troubles with lean4web, please DM me :smile: )

I think I have successfully installed lean but lean4web still not working I guess the issue is still somehow related to elan even if it is found on ym system. I have attached a screenshot for your reference.
image.png

[Jon Eugster]

I'll DM you to not spam everybody here!

[Jon Eugster]

Thanks for the report earlier @Mohamamd Awheeo! I updated the instructions to include npm run build_server now.