Where to get leanproject on Windows?

Stream: new members

[Jason He]

Hi, I installed lean3 via elan. But I cannot find leanproject. I am trying to run leanproject get tutorials. If I get tutorial manually from git, VSCode will report many errors including "increase memory consumption". If anyone can help point out where to download leanproject for Windows, I hope the problem can go away. Thanks

[Julian Berman]

Hi. Welcome. Did you follow the instructions from https://leanprover-community.github.io/install/windows.html

[Jason He]

I used elan and try to have lean3 and lean4 side by side. Now I followed the lean 3 installation instruction exactly. But the tutorial shows "Loading..." in the infoview window. It seems something still not right.

[Kevin Buzzard]

That might mean that your default elan toolchain is a lean 4 toolchain. Installing lean 4 before lean 3 might give you this. Alternatively it might mean you didn't open the root of the project directory using VS Code's "open folder" functionality

[Jason He]

My problem got solved by compiling mathlib locally. Once done, VSCode stopped "Loading ..." message.

[Kevin Buzzard]

Nice. You should never need to do this though.