Installation on macOS

Stream: new members

[Yuhang Lin]

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?

[Julian Berman]

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

[Julian Berman]

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

[Yuhang Lin]

*   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

[Bryan Gin-ge Chen]

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

[Yuhang Lin]

What does that mean? "Aggressive HOSTS file"

[Bryan Gin-ge Chen]

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?

[Bryan Gin-ge Chen]

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.

[Yuhang Lin]

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

[Bryan Gin-ge Chen]

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.

[Yuhang Lin]

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!

[Ryan Duan]

Hey everyone, I'm new to lean and I'm having trouble downloading it on my M1 mac, I'm wonderign if anyone has seen this error before
error: Not a valid ref: refs/remotes/origin/master
fatal: ambiguous argument 'refs/remotes/origin/master': unknown revision or path not in the working tree.
Use '--' to separate paths from revisions, like this:
'git <command> [<revision>...] -- [<file>...]'

[Riccardo Brasca]

I've moved your message to a better topic.

[Ryan Duan]

thanks

[Mauricio Collares]

What command did you type that resulted in this error message?

[Ryan Duan]

huh
it somehow worked and now it returns this
==> Searching for similarly named formulae...
Error: No similarly named formulae found.
==> Searching for a previously deleted formula (in the last month)...
Error: No previously deleted formula found.
==> Searching taps on GitHub...
Error: No formulae found in taps.
zsh: command not found: elan
zsh: command not found: elan
ryanduan@Ryans-Air ~ %
when i put this in the terminal
/usr/local/bin/brew install elan mathlibtools
elan toolchain install stable
elan default stable

[Ryan Duan]

i followed all the instructions for the m1 chip mac installation

[Mauricio Collares]

The brew package name is elan-init and not elan. I know this was fixed in the elan readme recently, but probably there are other places with the wrong package name.

[Mauricio Collares]

Indeed, the instructions here need updating.

[Bryan Gin-ge Chen]

Thanks! If you haven't already started, do you mind opening a PR via the link at the bottom of the page?

[Ryan Duan]

i see thanks, it still says "Warning: No available formula with the name "elan-init"

[Mauricio Collares]

Weird, it should have found https://formulae.brew.sh/formula/elan-init

[Ryan Duan]

unless i did something else wrong earlier

[Ryan Duan]

lemme try again

[Mauricio Collares]

Are you trying with /usr/local/bin/brew install elan-init?

[Ryan Duan]

yes

[Ryan Duan]

nah same things happen

[Ryan Duan]

i think my homebrew is broken
i can't install git

[Ryan Duan]

like brew install git gives me the same error

[Mauricio Collares]

I am not a Mac user, but perhaps you need to run brew update. I guess this can happen if you lost internet connectivity precisely when the list of formulas was supposed to be fetched for the first time? This could also explain the transient git error you saw earlier.

[Ryan Duan]

i tried again now it gives me this
The x86_64 architecture is required for this software.

[Ryan Duan]

lol
thanks for helping idk why it's like this

[Mauricio Collares]

Ryan Duan said:

i tried again now it gives me this
The x86_64 architecture is required for this software.

That is true, but /usr/local/bin/brew was supposed to be x86_64 if you installed brew using the window in which you executed arch -x86_64 zsh.

[Ryan Duan]

Ah yes, i tried outside.

[Ryan Duan]

I did it again normally and Warning: No available formula with the name "mathlibtools".
==> Searching for similarly named formulae...
Error: No similarly named formulae found.
==> Searching for a previously deleted formula (in the last month)...
Error: No previously deleted formula found.
==> Searching taps on GitHub...
Error: No formulae found in taps.
zsh: command not found: elan
zsh: command not found: elan
ryanduan@ryans-air ~ % lean

[Ryan Duan]

is what I get. It doesn't make sense that it can't find the commands

[Julian Berman]

What does brew update say?

[Ryan Duan]

Already up-to-date

[Ryan Duan]

when i do brew intall elan-init without the path, it says it can't be installed in ARM etc etc
but when I use the comman given it says it can't find elan

[Julian Berman]

That means your brew isn't an x86_64 one.

[Julian Berman]

What does type -a brew say?

[Ryan Duan]

brew is /opt/homebrew/bin/brew
brew is /usr/local/bin/brew
brew is /opt/homebrew/bin/brew
brew is /usr/local/bin/brew
brew is /opt/homebrew/bin/brew
brew is /usr/local/bin/brew

[Julian Berman]

(Your PATH is quite screwy it'd seem, it's got duplicates on it, but we can ignore that for now)

[Julian Berman]

What does /usr/local/bin/brew update say?

[Ryan Duan]

ok yeah, i downloded it over and over agian bc it kept not working

[Ryan Duan]

ill stop doing that

[Ryan Duan]

†Already up-to-date.

[Ryan Duan]

sorry for the delay I thought I sent that already, and thanks for helping

[Julian Berman]

No problem. Can you also share /usr/local/bin/brew config and /opt/homebrew/bin/brew config?

[Ryan Duan]

For the first:
HOMEBREW_VERSION: 3.5.10
ORIGIN: https://github.com/Homebrew/brew
HEAD: c5731faf8be1ddc1eeae4b162b88bd76318fc279
Last commit: 11 days ago
Core tap ORIGIN: https://github.com/Homebrew/homebrew-core
Core tap HEAD: (none)
Core tap last commit: never
Core tap branch: HEAD
HOMEBREW_PREFIX: /usr/local
HOMEBREW_CASK_OPTS: []
HOMEBREW_DISPLAY: /private/tmp/com.apple.launchd.rJw07MHbyt/org.xquartz:0
HOMEBREW_MAKE_JOBS: 8
Homebrew Ruby: 2.6.8 => /usr/local/Homebrew/Library/Homebrew/vendor/portable-ruby/2.6.8_1/bin/ruby
CPU: octa-core 64-bit westmere
Clang: 13.1.6 build 1316
Git: 2.32.1 => /Library/Developer/CommandLineTools/usr/bin/git
Curl: 7.79.1 => /usr/bin/curl
macOS: 12.5.1-x86_64
CLT: 13.4.0.0.1.1651278267
Xcode: 13.4 => /Users/ryanduan/Downloads/Xcode.app/Contents/Developer
Rosetta 2: true

---

For the second:
HOMEBREW_VERSION: 3.5.10
ORIGIN: https://github.com/Homebrew/brew
HEAD: c5731faf8be1ddc1eeae4b162b88bd76318fc279
Last commit: 11 days ago
Core tap ORIGIN: https://github.com/Homebrew/homebrew-core
Core tap HEAD: 24e9624907b9c3023ffd2c1574366a03ad2d8998
Core tap last commit: 33 minutes ago
Core tap branch: master
HOMEBREW_PREFIX: /opt/homebrew
HOMEBREW_CASK_OPTS: []
HOMEBREW_DISPLAY: /private/tmp/com.apple.launchd.rJw07MHbyt/org.xquartz:0
HOMEBREW_MAKE_JOBS: 8
Homebrew Ruby: 2.6.8 => /opt/homebrew/Library/Homebrew/vendor/portable-ruby/2.6.8_1/bin/ruby
CPU: octa-core 64-bit arm_firestorm_icestorm
Clang: 13.1.6 build 1316
Git: 2.37.3 => /opt/homebrew/bin/git
Curl: 7.79.1 => /usr/bin/curl
macOS: 12.5.1-arm64
CLT: 13.4.0.0.1.1651278267
Xcode: 13.4 => /Users/ryanduan/Downloads/Xcode.app/Contents/Developer
Rosetta 2: false

[Mauricio Collares]

Looks like https://github.com/Homebrew/discussions/discussions/501

[Mauricio Collares]

They suggest deleting the directory printed by /usr/local/bin/brew --repo homebrew/core and then running /usr/local/bin/brew tap homebrew/core

[Mauricio Collares]

(and then trying to install elan-init and mathlibtools again, of course)

[Ryan Duan]

Ok thank you so much! I'll try that in a sec because I'm in class right now

[Mauricio Collares]

Mauricio Collares said:

They suggest deleting the directory printed by /usr/local/bin/brew --repo homebrew/core and then running /usr/local/bin/brew tap homebrew/core

Try this before re-running /usr/local/bin/brew install elan-init mathlibtools .

[Mauricio Collares]

This StackOverflow answer says you should tell git your email address before proceeding too (by running git config --global user.email your@email.com). I will submit a PR to add it to instructions.

[Alberto Navarro Garmendia]

Mauricio Collares ha dicho:

This StackOverflow answer says you should tell git your email address before proceeding too (by running git config --global user.email your@email.com). I have submitted a PR to the community website to add this step to the instructions, but to be honest I don't see which git command executed by the Homebrew install script requires this.

I copypaste "git config --global user.email your@email.com" (with my email), nothing happens

I copypaste "/usr/local/bin/brew install elan-init mathlibtools" ant the terminal starts running and dysplays the following

"Running brew update --auto-update...
fatal: Could not resolve HEAD to a revision
==> Homebrew is run entirely by unpaid volunteers. Please consider donating:
https://github.com/Homebrew/brew#donations

==> Auto-updated Homebrew!
Updated 1 tap (homebrew/cask).

Warning: No available formula with the name "elan-init".
==> Searching for similarly named formulae...
Error: No similarly named formulae found.
==> Searching for a previously deleted formula (in the last month)...
Error: No previously deleted formula found.
==> Searching taps on GitHub...
Error: No formulae found in taps."

[Alberto Navarro Garmendia]

Mauricio Collares ha dicho:

Mauricio Collares said:

They suggest deleting the directory printed by /usr/local/bin/brew --repo homebrew/core and then running /usr/local/bin/brew tap homebrew/core

Try this before re-running /usr/local/bin/brew install elan-init mathlibtools .

Thank you very much for the help but: what exactly do you mean by re-running? Shall I start from point 1 again? Thanks in advance

[Mauricio Collares]

I don't think you need to start from point 1. The instructions I'm suggesting are:
1) Run /usr/local/bin/brew --repo homebrew/core. If it prints a directory that contains Homebrew-related stuff, delete it manually (make sure to inspect it before deleting, though!).
2) Run /usr/local/bin/brew tap homebrew/core.
3) Run /usr/local/bin/brew install elan-init mathlibtools.

[Alberto Navarro Garmendia]

Mauricio Collares ha dicho:

I don't think you need to start from point 1. The instructions I'm suggesting are:
1) Run /usr/local/bin/brew --repo homebrew/core. If it prints a directory that contains Homebrew-related stuff, delete it manually (make sure to inspect it before deleting, though!).
2) Run /usr/local/bin/brew tap homebrew/core.
3) Run /usr/local/bin/brew install elan-init mathlibtools.

Thank you so much, Mauricio, but I follow the instructions and it doesn't seem to run. At point 3) the Terminal returns

Warning: No available formula with the name "elan-init".
==> Searching for similarly named formulae...
Error: No similarly named formulae found.
==> Searching for a previously deleted formula (in the last month)...
Error: No previously deleted formula found.
==> Searching taps on GitHub...
Error: No formulae found in taps.

In any case, I feel I have already abused your help far too much.

I am on a very nice conference with Johan Commelin teaching us Lean, when I get back home I'll take an older laptop and install Lean on it. Thanks so much for your help :pray:

[Mauricio Collares]

I don't know why your Homebrew is not working, sorry for the bad instructions. I guess starting over could work, now that git is configured. Either way, enjoy the conference!

[Chris Lovett]

You can also play with Lean just with your web browser, see gitpod instructions on https://github.com/leanprover/lean4-samples

[Alberto Navarro Garmendia]

Chris Lovett ha dicho:

You can also play with Lean just with your web browser, see gitpod instructions on https://github.com/leanprover/lean4-samples

Thanx Chris, this is what I am currently doing now. Thx to both!

[Alberto Navarro Garmendia]

May I ask two a simple question?

First things first:

1) where should I ask basic begginer questions? i am not used to Zulipchat, and it seems to me that the hashtag " new memebrs" requires a subsubject (like this "installation on macOS") Should I write a new subject for every doubt or is there a place for them?

2) On the natural number game, function world, level 8/9, it can be solved copy-pasting the level 7/9 code, and therefore using the 'exact' command at the end instead of 'apply' as the tutorial suggest. In fact, Lean says "Proof complete" (so I found an element on the empty set :grinning_face_with_smiling_eyes: ) Clearly I am not understanding the meaning of the instructions 'apply' or 'exact' and the difference bewteen them.

[Ruben Van de Velde]

Yes, please create a new topic for independent questions

[Mario Carneiro]

No matter which tactics you use, you shouldn't be able to prove the empty set has an element so presumably you are either misunderstanding the statement or lean's response

[Mario Carneiro]

note that exact and apply are often interchangeable

[Mario Carneiro]

specifically, if it's the last step of the proof then usually either one works

[Mauricio Collares]

Mario Carneiro said:

No matter which tactics you use, you shouldn't be able to prove the empty set has an element so presumably you are either misunderstanding the statement or lean's response

Function World Level 8 asks you to prove (P → Q) → (Q → empty) → P → empty

[Alberto Navarro Garmendia]

And it actually returns "proof complete" by copying my solution of level 7/9, which is

intro f, intro g, intro p, have h:=g(f(p)), exact h,

No need to use "apply". Kind of weird...

[Mario Carneiro]

aha, yes that's expected behavior. You are proving that if P implies Q and Q is false then P is false

[Mario Carneiro]

so that means that assuming P leads to a contradiction ("the empty set has an element", as you said)

[Mario Carneiro]

but it's not like this is a proof of empty under no assumptions

[Mario Carneiro]

which would indeed be concerning

[Alberto Navarro Garmendia]

I think this time i got it right. I have a doubt though, what should I do to open Lean?

Lean does not appear in the "programs" folder.

[Mauricio Collares]

You open VS Code by typing code your/project/directory

[peihan]

Hello!I have tried to type '/bin/bash -c "$(curl -fsSL https://raw.githubusercontent.com/leanprover-community/mathlib4/master/scripts/install_macos.sh)" && source ~/.profile' in the terminal following macOS installation in the lean community, but resulted in the error message 'curl: (7) Failed to connect to raw.githubusercontent.com port 443: Connection refused
source: no such file or directory: /Users/sunpeihan/.profile'
How to deal with the condition?

[Floris van Doorn]

The first error sounds like you don't have an internet connection, or that it hiccupped. Just try again.
The second error is harmless. If you still get this error after the first step succeeds, just close and reopen the terminal, and then continue with the next steps.