Unable to create a New Project in VSCode/Lean4 using Mathlib

Stream: mathlib4

[Daniel Donnelly]

So I tried 4 times. Got same or similar error. Could it just be my internet connection? Do you have an alternative way to download Mathlib?

---

ERRORS:

curl --version

curl 8.13.0 (Windows) libcurl/8.13.0 Schannel zlib/1.3.1 WinIDN

Release-Date: 2025-04-02

Protocols: dict file ftp ftps http https imap imaps ipfs ipns mqtt pop3 pop3s smb smbs smtp smtps telnet tftp ws wss

Features: alt-svc AsynchDNS HSTS HTTPS-proxy IDN IPv6 Kerberos Largefile libz NTLM SPNEGO SSL SSPI threadsafe Unicode UnixSockets

git --version

git version 2.49.0.windows.1

Invoke-WebRequest -Uri "https://elan.lean-lang.org/elan-init.ps1" -OutFile "elan-init.ps1"

Set-ExecutionPolicy -ExecutionPolicy Unrestricted -Scope Process

$rc = .\elan-init.ps1 -NoPrompt 1 -DefaultToolchain leanprover/lean4:stable

del .\elan-init.ps1

exit $rc

info: downloading installer to C:\Users\fruit\AppData\Local\Temp\

info: default toolchain set to 'leanprover/lean4:stable'

c:\Users\fruit\OneDrive\Desktop\Lean4Chaser\lean4chaser> curl --version

curl 8.13.0 (Windows) libcurl/8.13.0 Schannel zlib/1.3.1 WinIDN

Release-Date: 2025-04-02

Protocols: dict file ftp ftps http https imap imaps ipfs ipns mqtt pop3 pop3s smb smbs smtp smtps telnet tftp ws wss

Features: alt-svc AsynchDNS HSTS HTTPS-proxy IDN IPv6 Kerberos Largefile libz NTLM SPNEGO SSL SSPI threadsafe Unicode UnixSockets

c:\Users\fruit\OneDrive\Desktop\Lean4Chaser\lean4chaser> git --version

git version 2.49.0.windows.1

c:\Users\fruit\OneDrive\Desktop\Lean4Chaser\lean4chaser> elan --version

elan 4.1.2 (58e8d545e 2025-05-26)

elan toolchain install leanprover-community/mathlib4:lean-toolchain

info: downloading https://releases.lean-lang.org/lean4/v4.24.0-rc1/lean-4.24.0-rc1-windows.tar.zst

Error(Download(Msg("error during download")), State { next_error: Some(Error { description: "Transferred a partial file", code: 18, extra: Some("end of response with 206125824 bytes missing") }), backtrace: InternalBacktrace { backtrace: None } })

error:

could not download file from '

https://releases.lean-lang.org/lean4/v4.24.0-rc1/lean-4.24.0-rc1-windows.tar.zst

' to '

C:\Users\fruit\.elan\tmp\d5rng3nxd69kyayg_file

'

info:

caused by: error during download

info: caused by: [18] Transferred a partial file (end of response with 206125824 bytes missing)

=> Operation failed. Exit code: 1.

c:\Users\fruit\OneDrive\Desktop\Lean4Chaser\lean4chaser> curl --version

curl 8.13.0 (Windows) libcurl/8.13.0 Schannel zlib/1.3.1 WinIDN

Release-Date: 2025-04-02

Protocols: dict file ftp ftps http https imap imaps ipfs ipns mqtt pop3 pop3s smb smbs smtp smtps telnet tftp ws wss

Features: alt-svc AsynchDNS HSTS HTTPS-proxy IDN IPv6 Kerberos Largefile libz NTLM SPNEGO SSL SSPI threadsafe Unicode UnixSockets

c:\Users\fruit\OneDrive\Desktop\Lean4Chaser\lean4chaser> git --version

git version 2.49.0.windows.1

c:\Users\fruit\OneDrive\Desktop\Lean4Chaser\lean4chaser> elan --version

elan 4.1.2 (58e8d545e 2025-05-26)

elan toolchain install leanprover-community/mathlib4:lean-toolchain

info: downloading https://releases.lean-lang.org/lean4/v4.24.0-rc1/lean-4.24.0-rc1-windows.tar.zst

Error(Download(Msg("error during download")), State { next_error: Some(Error { description: "Transferred a partial file", code: 18, extra: Some("end of response with 206125824 bytes missing") }), backtrace: InternalBacktrace { backtrace: None } })

error:

could not download file from '

https://releases.lean-lang.org/lean4/v4.24.0-rc1/lean-4.24.0-rc1-windows.tar.zst

' to 'C:\Users\fruit\.elan\tmp\4im7rrgwk7a6zmk3_file'

info: caused by: error during download

info: caused by: [18] Transferred a partial file (end of response with 206125824 bytes missing)

=> Operation failed. Exit code: 1.

c:\Users\fruit\OneDrive\Desktop\Lean4Chaser\lean4chaser> curl --version

curl 8.13.0 (Windows) libcurl/8.13.0 Schannel zlib/1.3.1 WinIDN

Release-Date: 2025-04-02

Protocols: dict file ftp ftps http https imap imaps ipfs ipns mqtt pop3 pop3s smb smbs smtp smtps telnet tftp ws wss

Features: alt-svc AsynchDNS HSTS HTTPS-proxy IDN IPv6 Kerberos Largefile libz NTLM SPNEGO SSL SSPI threadsafe Unicode UnixSockets

c:\Users\fruit\OneDrive\Desktop\Lean4Chaser\lean4chaser> git --version

git version 2.49.0.windows.1

c:\Users\fruit\OneDrive\Desktop\Lean4Chaser\lean4chaser> elan --version

elan 4.1.2 (58e8d545e 2025-05-26)

elan toolchain install leanprover-community/mathlib4:lean-toolchain

info: downloading https://releases.lean-lang.org/lean4/v4.24.0-rc1/lean-4.24.0-rc1-windows.tar.zst

Error(Download(Msg("error during download")), State { next_error: Some(Error { description: "Failure when receiving data from the peer", code: 56, extra: Some("Recv failure: Connection was reset") }), backtrace: InternalBacktrace { backtrace: None } })

error: could not download file from 'https://releases.lean-lang.org/lean4/v4.24.0-rc1/lean-4.24.0-rc1-windows.tar.zst' to 'C:\Users\fruit\.elan\tmp\3vk2ejp7rs2lfuhj_file'

info:

caused by: error during download

info: caused by: [56] Failure when receiving data from the peer (Recv failure: Connection was reset)

=> Operation failed. Exit code: 1.

c:\Users\fruit\OneDrive\Desktop\Lean4Chaser\lean4chaser> curl --version

curl 8.13.0 (Windows) libcurl/8.13.0 Schannel zlib/1.3.1 WinIDN

Release-Date: 2025-04-02

Protocols: dict file ftp ftps http https imap imaps ipfs ipns mqtt pop3 pop3s smb smbs smtp smtps telnet tftp ws wss

Features: alt-svc AsynchDNS HSTS HTTPS-proxy IDN IPv6 Kerberos Largefile libz NTLM SPNEGO SSL SSPI threadsafe Unicode UnixSockets

c:\Users\fruit\OneDrive\Desktop\Lean4Chaser\lean4chaser> git --version

git version 2.49.0.windows.1

c:\Users\fruit\OneDrive\Desktop\Lean4Chaser\lean4chaser> elan --version

elan 4.1.2 (58e8d545e 2025-05-26)

elan toolchain install leanprover-community/mathlib4:lean-toolchain

info: downloading https://releases.lean-lang.org/lean4/v4.24.0-rc1/lean-4.24.0-rc1-windows.tar.zst

Error(Download(Msg("error during download")), State { next_error: Some(Error { description: "Transferred a partial file", code: 18, extra: Some("end of response with 143211264 bytes missing") }), backtrace: InternalBacktrace { backtrace: None } })

error: could not download file from 'https://releases.lean-lang.org/lean4/v4.24.0-rc1/lean-4.24.0-rc1-windows.tar.zst' to 'C:\Users\fruit\.elan\tmp\hs6vmaq9oadmzfbh_file'

info: caused by: error during download

info: caused by: [18] Transferred a partial file (end of response with 143211264 bytes missing)

=> Operation failed. Exit code: 1.

[Kevin Buzzard]

(I am not an expert but this message would be more readable if you enclosed it within triple backticks. Are you getting an error on elan --version?

[Robin Arnez]

Yeah, I know this error. With a bad internet connection it just sometimes randomly interrupts the download (timeout or something?). I honestly have no clue how to solve it, you might be able to copy and unzip the file it downloads to the correct place though to make it work (in %USERPROFILE%\.elan\toolchains).