Installation on windows

Stream: new members

[Jovan Gerbscheid]

Hello, I installed lean using elan, but it isn't working. I installed the new version of python 3.10 and I installed vscode. When I open the introduction project in vscode, on the right in "lean infoview" where lean should be checking the proof, it just says "loading..."

[Yaël Dillies]

To precise, leanproject get-m on the tutorial project and leanproject get-c on mathlib don't print out anything.

[Kevin Buzzard]

Usually "loading" indicates that you didn't open the root directory of a correctly formatted lean project with VS Code's "open folder" functionality.

[Kevin Buzzard]

If that isn't it, can you confirm that you installed following the instructions on the community website rather than Microsoft's website?

[Jovan Gerbscheid]

I managed to install it successfully today after installing wsl

[Marco Campos]

Good evening everyone,
I have been trying to install LEAN locally on my windows computer by following the tutorial that was posted here: https://leanprover-community.github.io/install/windows.html
However, when I run 'pip3 install mathlibtools' I continue to get an error message :

Exception: ERROR: The 'make' utility is missing from PATH

---

ERROR: Failed building wheel for pynacl
Running setup.py clean for pynacl
Failed to build pynacl
ERROR: Could not build wheels for pynacl which use PEP 517 and cannot be installed directly

I've googled and looked through the tutorials but none of the solutions I've seen have worked. Anyone have any suggestions?