installation problems on M2 mac

Stream: general

[Ruiting Jiang]

Hi! I tried to install Lean 3 on an M2 mac following the instructions on the community website. Mathlibtools isn't working for me: the error I get is

% /usr/local/bin/brew install mathlibtools
Error: Cannot install in Homebrew on ARM processor in Intel default prefix (/usr/local)!
Please create a new installation in /opt/homebrew using one of the
"Alternative Installs" from:
  https://docs.brew.sh/Installation
You can migrate your previously installed formula list with:
  brew bundle dump
jiangruiting@jiangruitingdeMacBook-Pro xena-workshop-set-families %

Any ideas? Thanks in advance

[Ruiting Jiang]

Progress: I wasn't in the x86 shell. Now I have this:

% leanproject get YaelDillies/xena-workshop-set-families
Cloning from git@github.com:YaelDillies/xena-workshop-set-families.git
Error cloning via SSH, trying HTTPS...
Cloning from https://github.com/YaelDillies/xena-workshop-set-families.git
configuring xena-workshop-set-families 0.1
mathlib: trying to update _target/deps/mathlib to revision ebf8ff42db1e71dd0880e3f274dd5ac9303b8a2a
> git fetch    # in directory _target/deps/mathlib
> git checkout --detach ebf8ff42db1e71dd0880e3f274dd5ac9303b8a2a    # in directory _target/deps/mathlib
fatal: reference is not a tree: ebf8ff42db1e71dd0880e3f274dd5ac9303b8a2a
external command exited with status 128
Command '['leanpkg', 'configure']' returned non-zero exit status 1.
jiangruiting@dyn897-234 Xena %

I'm close! (PS this is actually Kevin Buzzard talking, I'm trying to get a student set up)

[Ruiting Jiang]

(ok got it -- Yael's project has got an invalid toml!)

[Kevin Buzzard]

Sorry for the noise. This is now resolved. Yael's lean set-up is a bit broken and he managed to create a corrupted project somehow.

[Kind Bubble]

I haven't been able to install lean 4 on my new M2 Mac.

When I try to install Rosetta with

softwareupdate --install-rosetta

I get:

Installing Rosetta 2 on this system is not supported.

[Kind Bubble]

/usr/local/bin/brew install mathlibtools

gives

Running `brew update --auto-update`...
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>...]'

[Alistair Tucker]

I think you shouldn't need Rosetta for Lean 4.

[Alistair Tucker]

Or mathlibtools