Installation help

Stream: Lean for Scientists and Engineers 2024

[Christian Tzurcanu]

problem creating a project with lean4 and mathlib on MAcOSX:

Cannot update dependencies. Command output: info: lean_t: no previous manifest, creating one from scratch info: leanprover-community/mathlib: cloning https://github.com/leanprover-community/mathlib4 to '././.lake/packages/mathlib' error: external command 'git' exited with code 128

[Tyler Josephson ⚛️]

Here's a thread for getting help with installation

[Notification Bot]

A message was moved here from #Lean for Scientists and Engineers 2024 > Lean files for class by Tyler Josephson ⚛️.

[Christian Tzurcanu]

tried to move it here: i was too late

[Christian Tzurcanu]

sorry: i did not understand how threads are rendered in this interface

[Tyler Josephson ⚛️]

No worries! I'm not sure about this error. But stick around and I'm sure someone who knows will come help. Thanks for joining today!

[Christian Tzurcanu]

i should mention: git is installed ok

[Tyler Josephson ⚛️]

Christian Tzurcanu said:

sorry: i did not understand how threads are rendered in this interface

If you click on a thread under the channel, it'll narrow to just the messages in the thread.

[Christian Tzurcanu]

macOSX Sonoma 14.6 Beta (23G5061b) Xcode Version 15.4 (15F31d)

[Christian Tzurcanu]

CLI tools installed

[Christian Tzurcanu]

git error code 128 seems to happen when:

• The remote repository does not exist. If the remote repository that you are trying to fetch from does not exist, git fetch will fail with exit code 128.
• The remote repository is not accessible. If you do not have permission to access the remote repository, git fetch will fail with exit code 128.
• The remote repository is corrupt. If the remote repository is corrupt, git fetch will fail with exit code 128.

[Christian Tzurcanu]

so i do not understand why i'd have this problem alone. this should happen for all who want to install mathlib now

[Matthew Ballard]

What does

git clone https://github.com/leanprover-community/mathlib4 --verbose

return?

[Christian Tzurcanu]

Cloning into 'mathlib4'...
POST git-upload-pack (175 bytes)
POST git-upload-pack (gzip 158352 to 78671 bytes)
remote: Enumerating objects: 478840, done.
remote: Counting objects: 100% (8473/8473), done.
remote: Compressing objects: 100% (4150/4150), done.

and loading

[Christian Tzurcanu]

remote: Compressing objects: 100% (4150/4150), done.
error: RPC failed; curl 56 Recv failure: Connection reset by peer
error: 5355 bytes of body are still expected
fetch-pack: unexpected disconnect while reading sideband packet
fatal: early EOF
fatal: fetch-pack: invalid index-pack output

!!!

[Christian Tzurcanu]

so you mean that i should try until there is no early EOF?

[Christian Tzurcanu]

(i am at the 5th try)

[Matthew Ballard]

Hmm. It works fine for me. Is there anything particular about your network that might be problematic for connections to github?

[Christian Tzurcanu]

i got a VPN. i will try without ASAP

[Matthew Ballard]

That is possible. Github could be blocking some VPN traffic

[Christian Tzurcanu]

yes. that was it. could not imagine that it would be a problem. thank you Matthew!

[Dhruva Sambrani]

I followed the installation guide from Mathlib github (Use as dependancy), but I still get mathlib not installed (or something similar) when I lean --run Lecture1.lean.

(Using elan)

[Dhruva Sambrani]

When I run lake exe cached get, it runs well

[Dhruva Sambrani]

So it is not a net issue

[Dhruva Sambrani]

I think the #mathlib4 channel says mathlib on lean4 is not well developed enough?

[Shreyas Srinivas]

I don't understand where you get that idea

[Simon Beaumont]

I don't think you should run lean --run unless you have a main.lean -- you just need to open the lean file in vscode.

[Floris van Doorn]

Dhruva Sambrani said:

I think the #mathlib4 channel says mathlib on lean4 is not well developed enough?

Where did you see this? This information is at least a year old. If you see it in current documentation/descriptions, we would like to remove it.

[Dhruva Sambrani]

Yes i'm sorry, this was 1.5 years ago lol.

[Dhruva Sambrani]

https://github.com/leanprover/lean4/issues/1792#issuecomment-1302339734 I jumped from this comment, which was even older. My bad

[Dhruva Sambrani]

Simon Beaumont said:

I don't think you should run lean --run unless you have a main.lean -- you just need to open the lean file in vscode.

So how would one check if the proofs are correct without using VSCode?

[Simon Beaumont]

I use emacs but that's another story -- Lean is very interactive - you need to be using some form of IDE I think.

[Kevin Buzzard]

You can run lean in a browser, that's another solution. For example if you want to work on Lecture2.lean you can just paste it directly into the web page at https://live.lean-lang.org/ .