Install lean4 on windows

Stream: new members

[Tiffany]

Hello community, I am new to lean and want to install lean4 on my computer. I followed the instruction here install/windows and successfully installed VS code, git, lean4 extension and set up elan and lean. But as I followed the instructions here install/project about working on Lean project, I was stuck at the first step: every time when I type "source ~/.profile" into Git Bash, the Git Bash says "/c/Users/ASUS/.profile: No such file or directory", I don't know how to fix it since I know little about computer science. Can someone help me? Any help is appreciated!

[Bbbbbbbbba]

Have you tried skipping this step (since the guide says it depends on your OS)?

[Jad Abou Hawili]

Skipping installing lean is an option as well, https://live.lean-lang.org/
source ~/.profile step is for mac,linux, and unix like stuff. skip it if your on windows

[Jon Eugster]

Indeed, instead of that first step, you can also just restart (or logout&login to) your computer, or it might work without anything. It's just to ensure your computer knows all the correct paths where things are installed.

I made a Pull Request that adds (or simply restart your computer)at the end of that step: https://github.com/leanprover-community/leanprover-community.github.io/pull/488

[Tiffany]

Bbbbbbbbba said:

Have you tried skipping this step (since the guide says it depends on your OS)?

Sorry for taking so long to reply. Actually I tried it before, but I was still stuck at the fifth step: after I type "git clone https://github.com/leanprover-community/mathematics_in_lean.git" into Git Bash, I successfully clone the folder called "mathematics_in_lean" to my computer at the location "C:\Users\ASUS", and the command "cd mathematics_in_lean" also works as well. But when I typed "lake exe cache get", the Git Bash replies me with the following message:
5e435570ff6405c87de195ea0b69717.png

[Tiffany]

Jad Abou Hawili said:

Skipping installing lean is an option as well, https://live.lean-lang.org/
source ~/.profile step is for mac,linux, and unix like stuff. skip it if your on windows

It sounds like a good suggestion. Maybe I should try the online version.

[Jon Eugster]

I think the first thing to try is lake clean and then lake exe cache get again. The error sounds a bit as if downloading mathlib got interrupted or so.

Alternatively, one can also delete the folder mathematics_in_lean\.lake\ and then try again

[Tiffany]

Jon Eugster said:

I think the first thing to try is lake clean and then lake exe cache get again. The error sounds a bit as if downloading mathlib got interrupted or so.

Alternatively, one can also delete the folder mathematics_in_lean\.lake\ and then try again

Yeah, I follow your advice and delete the folder mathematics_in_lean\.lake\ and try again. At this moment things become different: After I type cd mathematics_in_lean followed by lake exe cache get, the command works partly and starts to cloning https://github.com/leanprover-community/mathlib4 to .\.lake/packages\mathlib, but the Git Bash still replies with two errors as follows:
b4c950960536599347404140107b759.png

[Ruben Van de Velde]

Have you run lake update at some point?

[Ruben Van de Velde]

Because this is an error that should not happen if you have a clean clone

[Jon Eugster]

What Ruben says. I think this can be debugged by either seeing the output of

git diff

or seeing the content of your files lean-toolchain and further maybe lakefile.lean and lake-manifest.json. (all inside the mathematics_in_lean directory)

[Tiffany]

Ruben Van de Velde said:

Have you run lake update at some point?

Yes, I have run it before...

[Ruben Van de Velde]

Why?

[Tiffany]

Ruben Van de Velde said:

Why?

At that moment I was following another instruction (here https://subfish-zhou.github.io/theorem_proving_in_lean4_zh_CN/setup.html) to install lean4, which says to get the Mathlib installed, one should run with the following command at the terminal

lake update
lake exe cache get

[Ruben Van de Velde]

I see. That's bad advice, unfortunately

[Ruben Van de Velde]

You can follow these instructions: https://leanprover-community.github.io/install/project.html#working-on-an-existing-project

[Ruben Van de Velde]

That is, I recommend removing your current clone of MIL and starting again from there

[Tiffany]

(deleted)

[Tiffany]

Ruben Van de Velde said:

That is, I recommend removing your current clone of MIL and starting again from there

I take your advice and start again, but it seems that the same problem still exists...
4252cdd4ed34cc6f0f238d7b72203de.png

[Tiffany]

Jon Eugster said:

What Ruben says. I think this can be debugged by either seeing the output of

git diff

or seeing the content of your files lean-toolchain and further maybe lakefile.lean and lake-manifest.json. (all inside the mathematics_in_lean directory)

I try it just now and the Git Bash replies with a large amount of message that I don't understand...
1.png
I also attach the three files lean-toolchain, lakefile.lean, lake-manifest.json in mathematics_in_lean below.
lakefile.lean
lake-manifest.json
lean-toolchain

[Jon Eugster]

sorry, I should have specified more clearly :) you want to first cd into your directory and then do git diff in there. (but hopefully that will not print anything). There is nothing for you to do outside the directory except the initial git clone & cd which you do in all other screenshots :)

Regardless, I don't spot a missmatch in the toolchain & manifest right away, so I don't know what's up...

[Tiffany]

Jon Eugster said:

sorry, I should have specified more clearly :) you want to first cd into your directory and then do git diff in there. (but hopefully that will not print anything). There is nothing for you to do outside the directory except the initial git clone & cd which you do in all other screenshots :)

Regardless, I don't spot a missmatch in the toolchain & manifest right away, so I don't know what's up...

Yeah, it produces nothing...
b8f28e5cbb2ced3f9e976a73d54451c.png

[Ruben Van de Velde]

Okay, and now lake exe cache get

[Tiffany]

Ruben Van de Velde said:

Okay, and now lake exe cache get

Do you mean run the command lake exe cache get again? In the last reply I have run it and the Git Bash replies me with the same errors... And I run it again just now, but the problem remains unchanged...
b9b8a8fe1ba5c218bc8e95387659fae.png

[Ruben Van de Velde]

That's odd. Can you also run git status and git show?

[Tiffany]

Maybe I solved my problem: instead of cloning the folder mathematics_in_lean on C disk, I clone it to the D disk, and the instruction here https://leanprover-community.github.io/install/project.html works very well. I think the following screenshot indicates this.
d5ef139d92da69e0e834cae6694c453.png
But actually I don't know what the underlying principle is...

[Tiffany]

Ruben Van de Velde said:

That's odd. Can you also run git status and git show?

Thank you for reply me at such a late time. I run them, and the following is the feedback.
1.png
2.png