Unable to create project using mathlib in WSL 1

Stream: new members

[Qinshi Wang]

I get the following error message:

lean/new_math1> lean +leanprover-community/mathlib4:lean-toolchain --version
thread 'main' panicked at src/elan-utils/src/utils.rs:472:32:
called `Result::unwrap()` on an `Err` value: Error { description: "Couldn't resolve host name", code: 6, extra: Some("Could not resolve host: github.com") }
note: run with `RUST_BACKTRACE=1` environment variable to display a backtrace
=> Operation failed. Exit code: 101.

But I can access github.com e.g. curl https://github.com looks fine.

[Kevin Buzzard]

Are you on windows? Did you try disabling your antivirus?

[Qinshi Wang]

Yes. I'm using WSL 1 on Windows. I'm not using any antivirus except Windows itself. I don't think Windows' protection blocks Github.

[Kevin Buzzard]

Well something is blocking GitHub I guess...

[Julian Berman]

Yes this is going to be some not-really-Lean-related networking issue typically, often you being man-in-the-middled by some entity, and then your curl has been modified to deal with that.

[Julian Berman]

A concrete first suggestion would be to do what the error says, run RUST_BACKTRACE=1 lean +...etc. A second suggestion would be to run dig github.com and/or nslookup github.com.

[Derek Rhodes]

For another data point, I setup WSL1 Debian inside of a windows guest, running inside virtualbox on a linux host. @Qinshi Wang, I tried the lean command you provided and, for what its worth, it does work.

win11:/mnt/c/Users/derek$ lean +leanprover-community/mathlib4:lean-toolchain --version
Lean (version 4.19.0-rc2, x86_64-unknown-linux-gnu, commit fafd381c9059, Release)

[Qinshi Wang]

From @Derek Rhodes's comment, it is clear that there is a network connection issue. The reason is not clear. I'm in HK, not mainland China. I tried the diagnosis suggested above.
The result of dig github.com looks normal:

$ dig github.com

; <<>> DiG 9.16.1-Ubuntu <<>> github.com
;; global options: +cmd
;; Got answer:
;; ->>HEADER<<- opcode: QUERY, status: NOERROR, id: 45191
;; flags: qr rd ra; QUERY: 1, ANSWER: 1, AUTHORITY: 0, ADDITIONAL: 1

;; OPT PSEUDOSECTION:
; EDNS: version: 0, flags:; udp: 512
;; QUESTION SECTION:
;github.com.                    IN      A

;; ANSWER SECTION:
github.com.             60      IN      A       20.205.243.166

;; Query time: 17 msec
;; SERVER: 10.30.0.2#53(10.30.0.2)
;; WHEN: Mon Apr 07 02:50:22 CST 2025
;; MSG SIZE  rcvd: 55

But nslookup github.com looks strange, that it returns a valid IP address but shows connection timed out. But I can ping the IP address and visit it in the browser.

$ nslookup github.com
Server:         10.30.0.2
Address:        10.30.0.2#53

Non-authoritative answer:
Name:   github.com
Address: 20.205.243.166
;; connection timed out; no servers could be reached

[Julian Berman]

20.205.243.166 looks like it probably is the right IP from where you are. You could check mtr 20.205.243.166 perhaps, which will tell you if somewhere in between you and GitHub is dropping your packets -- you could also check to see how your browser is configured in terms of proxy settings. It looks like maybe you're on a university network? You might also be able to ask them what's up. You can also run curl -v github.com and see if where it ends up talking to matches that IP or not. None of the above is Lean related though so others may recommend you look elsewhere to solve your issue and come back when it's fixed!