Zulip Chat Archive

Stream: new members

Topic: Installation on macOS


view this post on Zulip Yuhang Lin (Oct 08 2020 at 03:22):

I tried to download lean on macOS in "terminal" by the code

/bin/bash -c "$(curl -fsSL https://raw.githubusercontent.com/leanprover-community/mathlib-tools/master/scripts/install_macos.sh)" && source ~/.profile

However the error code:

curl: (7) Failed to connect to raw.githubusercontent.com port 443: Connection refused

keeps jumping out.

I tried to install homebrew to help me but the same error code is displayed. Are there other ways to install lean on macOS? Or is there a way to fix this problem?

view this post on Zulip Julian Berman (Oct 08 2020 at 03:26):

Hi! That sounds odd. Are you in behind some corporate networking environment or something perhaps?

view this post on Zulip Julian Berman (Oct 08 2020 at 03:26):

Can you show what curl -v https://raw.githubusercontent.com shows you

view this post on Zulip Yuhang Lin (Oct 08 2020 at 03:51):

*   Trying 0.0.0.0:443...
* Connection failed
* connect to 0.0.0.0 port 443 failed: Connection refused
* Failed to connect to raw.githubusercontent.com port 443: Connection refused
* Closing connection 0
curl: (7) Failed to connect to raw.githubusercontent.com port 443: Connection refused

view this post on Zulip Bryan Gin-ge Chen (Oct 08 2020 at 03:57):

For some reason your computer is redirecting https://raw.githubusercontent.com to localhost. Do you have an overly aggressive HOSTS file perhaps?

view this post on Zulip Yuhang Lin (Oct 08 2020 at 03:59):

What does that mean? "Aggressive HOSTS file"

view this post on Zulip Bryan Gin-ge Chen (Oct 08 2020 at 04:01):

Ah, I guess it may not have been something you set up yourself, but see this page.

Maybe Julian's question is more comprehensible:

Are you in behind some corporate networking environment or something perhaps?

view this post on Zulip Bryan Gin-ge Chen (Oct 08 2020 at 04:03):

Here's the start of what I see when I run curl -V https://raw.githubusercontent.com:

*   Trying 151.101.64.133:443...
* TCP_NODELAY set
* Connected to raw.githubusercontent.com (151.101.64.133) port 443 (#0)
* ALPN, offering http/1.1

My computer tries the actual IP of https://raw.githubusercontent.com, not 0.0.0.0 which is the IP of your own computer. Often sites get redirected to 0.0.0.0 when they are blocked by HOSTS or some other mechanism.

view this post on Zulip Yuhang Lin (Oct 08 2020 at 04:08):

I am on my private network, and my IPv4 address is 192.168.124.6. Can changing the IP address manually help?

view this post on Zulip Bryan Gin-ge Chen (Oct 08 2020 at 04:21):

Are you able to access https://raw.githubusercontent.com/leanprover-community/mathlib-tools/master/scripts/install_macos.sh in your browser? If so, I found some people discussing a similar issue here, but I don't know if it's applicable to your situation as I don't have much experience with VPNs.

view this post on Zulip Yuhang Lin (Oct 08 2020 at 04:47):

Allright, I think it is a problem with Great Fire Wall and maybe I could try to switch to another VPN. Thank you very much!


Last updated: May 14 2021 at 03:27 UTC