Installation on mac issue

Stream: new members

[Jérémie Turcotte]

I'm trying to get a copy of mathlib using "leanproject get mathlib" but getting error "info: downloading component 'lean'
error: binary package was not provided for 'darwin'"
Not sure what to do. I am on an M1 mac if that is helpful. Thanks

[Kevin Buzzard]

elan self update should fix this error.

[Kevin Buzzard]

Github changed the way that things were stored and broke elan, so anyone who installed elan more than a month or two ago unfortunately needs to update it manually (or, if my suggestion doesn't work, re-install it).

[Matthew Ballard]

Did you install lean via rosetta?

[Kevin Buzzard]

I am still unclear about how method of installation relates to whether elan self update succeeds.

[Matthew Ballard]

Elan has M1 binaries. Lean 3 doesn't.

[Matthew Ballard]

I get error: self-update is disabled for this build of elan for example because I installed it via nix packages.

[Jérémie Turcotte]

I indeed had the self-update disabled issue, but reinstalled everything fresh and now it works! Thanks alot