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?

[Yitzhak Zangi]

Is there anything to run instead of source .profile in Windows ?

[Julian Berman]

Can you elaborate a bit? Are you saying you ran the installation script on windows and elan isn't working for you?

[Yitzhak Zangi]

No, I just read this page, and this is the 1st instruction.
So what shall I do when working with Windows?

[Julian Berman]

Have you already installed Lean then? That page (and line) is for after you do.

[Yitzhak Zangi]

of course. I'm sorry that it wasn't evident.

[Julian Berman]

OK, and if you open a terminal and run lean --version, what do you see?

[Yitzhak Zangi]

4.4.0

[Julian Berman]

Great, everything probably is working then, just skip that line and continue forward.

[Yitzhak Zangi]

thanks. so maybe one should add this as a comment?

[Julian Berman]

It's a bit tersely written when it says "you may need to" if you don't already know how to check whether you need to -- so perhaps. I'm sure a pull request wouldn't be unwelcome to add a few more words there.