M1 Macs: Installing the Lean 3 toolchain

Stream: new members

[Trevor Fancher]

Installing Lean on an M1 based Mac

Changelog

• 21 September 2021 - First version. Known to work on my M1 MacBook Air running Big Sur (macOS 11.6 build 20G165)

Install brew and leanproject

Install Homebrew by running the following command in in Terminal.app (found in the /Applications/Utilities/ folder)

/bin/bash -c "$(curl -fsSL https://raw.githubusercontent.com/Homebrew/install/HEAD/install.sh)"

Now run the following command to install leanproject. This may take a few minutes because the mathlibtools packages has many dependecies that brew will automatically install.

brew update
brew install mathlibtools

Install elan from source

Do not install elan from brew. It won't work. Instead, we must build it from source. Start by installing some dependencies

brew install git
brew install gmp
brew install coreutils
brew install rust

Now we need to get the sources. I put most things like this in my ~/repos folder, but feel free to put the sources where you want. (Note that v1.0.8 is the newest release of elan, but it fails with the following error message, so v1.0.7 it is for now)

elan v1.0.8 error message

error: failed to run custom build command for elan-dist v1.11.0 (/Users/trevor/repos/elan/src/elan-dist)

Caused by:
process didn't exit successfully: /Users/trevor/repos/elan/target/debug/build/elan-dist-cf4fa37c4a1b6d17/build-script-build (exit status: 101)
--- stderr
thread 'main' panicked at 'called Result::unwrap() on an Err value: NotPresent', src/elan-dist/build.rs:8:50
note: run with RUST_BACKTRACE=1 environment variable to display a backtrace

mkdir -p ~/repos/
cd ~/repos
git clone https://github.com/leanprover/elan.git
git checkout v1.0.7
cd elan

Now we need to build and install elan. The cargo command comes from installing rust above. It builds and pulls in the dependencies for elan.

cargo build
cargo install
cd target/release/
./elan-init

You'll probably just want to "Proceed with installation (default)" by pressing 1 then the return key. Now run

source $HOME/.elan/env

so that your current Terminal session can find elan. This won't be neccesary in any newly open Terminal sessions.

Replace the Lean binaries

If you type lean in your Terminal you will get an error. While most apps work fine under Apple's emulation layer, for some reason lean and/or brew work together to confuse the emulation. So what we are going to do is build lean and its related commands from source and replace those files in the folder where elan stores its various binaries. Here we go:

cd ~/repos/
git clone https://github.com/leanprover-community/lean.git
cd lean
cat ~/.elan/update-hashes/stable

You should see something like https://github.com/leanprover-community/lean/releases/tag/v3.33.0 printed out now. Take the last part after the /tag/ (here it is v3.33.0) and run

git checkout v3.33.0
mkdir -p build/release
cd build/release
brew install cmake
cmake ../../src
make

This takes only 6 minutes with your new fancy M1 chip. Now we copy the built files where elan can find them. Note, you may have to type y to confirm deleting the Lean files.

cd ../../
rm ~/.elan/toolchains/stable/bin/lean
rm ~/.elan/toolchains/stable/bin/leanchecker
rm ~/.elan/toolchains/stable/bin/leanpkg
cp bin/lean ~/.elan/toolchains/stable/bin
cp bin/leanpkg ~/.elan/toolchains/stable/bin
cp build/release/checker/leanchecker ~/.elan/toolchains/stable/bin

You should be able to run

lean -v
leanchcker -v
leanpkg -v

to verify everything is running correctly. Congratulations, you have lean installed now.

Install VSCode

You may want to run

brew install --cask visual-studio-code
code --install-extension jroesch.lean

to get VSCode and the Lean extension installed.

Install other Lean version

Lets say you run

mkdir -p ~/projects/
cd ~/projects/
leanproject get ImperialCollegeLondon/formalising-mathematics

so that you can install the wonderful Formalising Mathematics workshop files. When doing this you'll get the error

dyld: Library not loaded: /usr/local/opt/gmp/lib/libgmp.10.dylib
  Referenced from: /Users/trevor/.elan/toolchains/leanprover-community--lean---3.24.0/bin/lean
  Reason: image not found
Command '['leanpkg', 'configure']' died with <Signals.SIGABRT: 6>.

because this Lean project requires a different version of Lean that we installed before. To fix this, we may do the following (note the leanprover-community--lean---3.24.0 part from the error message)

cat ~/.elan/update-hashes/leanprover-community--lean---3.24.0

which, unsurprisingly, tells us that the correct git tag is v3.24.0 for this version of Lean. So now we run

cd ~/repos/lean
git checkout v3.24.0
mkdir -p build/release
cd build/release
brew install cmake
cmake ../../src
make

and wait about 6 more minutes for Lean to build. Then we run

cd ../../
rm ~/.elan/toolchains/leanprover-community--lean---3.24.0/bin/lean
rm ~/.elan/toolchains/leanprover-community--lean---3.24.0/bin/leanchecker
rm ~/.elan/toolchains/leanprover-community--lean---3.24.0/bin/leanpkg
cp bin/lean ~/.elan/toolchains/leanprover-community--lean---3.24.0/bin
cp bin/leanpkg ~/.elan/toolchains/leanprover-community--lean---3.24.0/bin
cp build/release/checker/leanchecker ~/.elan/toolchains/leanprover-community--lean---3.24.0/bin

and now we have Lean 3.24.0 installed as well. I recommend first deleting the failed formalising-mathematics folder from before before continuing. So something like

cd ~/projects/
rm -rf formalising-mathematics
leanproject get ImperialCollegeLondon/formalising-mathematics
code formalising-mathematics

and you should be up and running.

[Chiu Tim]

When deleting the Lean files here, I get the error message No such file or directory

lean % cd ../../
rm ~/.elan/toolchains/stable/bin/lean
rm ~/.elan/toolchains/stable/bin/leanchecker
rm ~/.elan/toolchains/stable/bin/leanpkg
cp bin/lean ~/.elan/toolchains/stable/bin
cp bin/leanpkg ~/.elan/toolchains/stable/bin
cp build/release/checker/leanchecker ~/.elan/toolchains/stable/bin
override r-xr-xr-x timchiu/staff for /Users/timchiu/.elan/toolchains/stable/bin/lean? y
override r-xr-xr-x timchiu/staff for /Users/timchiu/.elan/toolchains/stable/bin/leanchecker? y
override r-xr-xr-x timchiu/staff for /Users/timchiu/.elan/toolchains/stable/bin/leanpkg? y
cp: bin/lean: No such file or directory
cp: bin/leanpkg: No such file or directory
cp: build/release/checker/leanchecker: No such file or directory

Any help would be appreciated

[Kevin Buzzard]

don't delete the Lean files?

[Scott Morrison]

Kevin is saying: we don't know what you're doing, or why. Please give us some context.

[Kevin Buzzard]

I can tell you what the errors mean -- cp bin/lean ~/.elan/toolchains/stable/bin means "make a copy of the file bin/lean some place or other" and the error cp: bin/lean: No such file or directory means "...but there is no file bin/lean so I can't do this"

[Kevin Buzzard]

aah got it -- you're cutting and pasting some code from the post above! Perhaps my last message is helpful then. You need your working directory to be in a place where there's a directory called bin with a file called lean in it.

[Kevin Buzzard]

You might want to post the output of pwd and ls -al, maybe all that's happening is that things are fine but you're in the wrong directory for some reason.

[Chiu Tim]

timchiu@192 lean % pwd
/Users/timchiu/repos/lean
timchiu@192 lean % ls -al
total 72
drwxr-xr-x 22 timchiu staff 704 30 Oct 10:17 .
drwxr-xr-x 4 timchiu staff 128 30 Oct 10:15 ..
-rw-r--r-- 1 timchiu staff 49 30 Oct 10:15 .clang-format
-rw-r--r-- 1 timchiu staff 153 30 Oct 10:15 .codecov.yml
drwxr-xr-x 12 timchiu staff 384 30 Oct 10:47 .git
-rw-r--r-- 1 timchiu staff 27 30 Oct 10:15 .gitattributes
drwxr-xr-x 5 timchiu staff 160 30 Oct 10:15 .github
-rw-r--r-- 1 timchiu staff 315 30 Oct 10:15 .gitignore
-rw-r--r-- 1 timchiu staff 9160 30 Oct 10:15 LICENSE
-rw-r--r-- 1 timchiu staff 3322 30 Oct 10:15 README.md
drwxr-xr-x 7 timchiu staff 224 30 Oct 10:21 bin
-rw-r--r-- 1 timchiu staff 308 30 Oct 10:15 bors.toml
drwxr-xr-x 3 timchiu staff 96 30 Oct 10:17 build
drwxr-xr-x 14 timchiu staff 448 30 Oct 10:15 doc
drwxr-xr-x 3 timchiu staff 96 30 Oct 10:15 extras
drwxr-xr-x 4 timchiu staff 128 30 Oct 10:15 images
drwxr-xr-x 7 timchiu staff 224 30 Oct 10:15 leanpkg
drwxr-xr-x 9 timchiu staff 288 30 Oct 10:15 library
drwxr-xr-x 28 timchiu staff 896 30 Oct 10:15 script
drwxr-xr-x 19 timchiu staff 608 30 Oct 10:15 src
drwxr-xr-x 4 timchiu staff 128 30 Oct 10:15 tests
drwxr-xr-x 12 timchiu staff 384 30 Oct 10:15 tmp

[Chiu Tim]

Kevin Buzzard said:

aah got it -- you're cutting and pasting some code from the post above! Perhaps my last message is helpful then. You need your working directory to be in a place where there's a directory called bin with a file called lean in it.

Yes, I am just copying code and I have no idea what any this means :joy:

[Jason Rute]

When you get this working, since I assume you are on a new M1 pro/max chip, I’d love to hear how long that make step above took.

[Tim Chiu]

Yes I'm on the M1 pro, it took 5 minutes and 20 seconds

[Kevin Buzzard]

So it looks like you have a bin directory. What does ls -l bin/ return?

[Tim Chiu]

No such file or directory

[Kevin Buzzard]

yeah but before you had a bin directory

[Kevin Buzzard]

do you know about the command line? Sorry if I'm telling you things you already know

[Kevin Buzzard]

You can navigate around through directories etc on a mac using a file explorer. I think the mac one is called "finder"? At any point the explorer is "in" a given directory, and you can go into subdirectories and back up out of them etc

[Kevin Buzzard]

The command line is just the same. You typed a command cp bin/lean ~/.elan/toolchains/stable/bin, which means "copy a file into a directory", and it didn't work, the error was cp: bin/lean: No such file or directory. Either that file is somewhere on your system and we can try to find it, or the file is not on your system and something went wrong earlier.

[Kevin Buzzard]

The thing about bin/lean is that it is a relative path. It means "start where we are now, then go into the bin directory and get the file called lean in that directory".

[Kevin Buzzard]

So for example if you close your terminal and then open it again, you're screwed, because when you open a new terminal it won't be pointing to the directory which your old terminal was in.

[Kevin Buzzard]

This is why it's funny that you're telling me the error 2 days after our last conversation, because on my computer most terminals don't last two days

[Kevin Buzzard]

If you open a new terminal, and type cd /Users/timchiu/repos/lean and then cd bin and then ls, what happens?

[Tim Chiu]

Right! I got :
lean lean-gdb.py leanpkg leanpkg.bat

[Kevin Buzzard]

Oh great -- lean is there! So go back up with cd /Users/timchiu/repos/lean again and then try cutting and pasting precisely the part which didn't work before, i.e.:

cp bin/lean ~/.elan/toolchains/stable/bin
cp bin/leanpkg ~/.elan/toolchains/stable/bin
cp build/release/checker/leanchecker ~/.elan/toolchains/stable/bin

If this works then you can continue with the instructions. But don't ever close your terminal and then come back to it later because this action will move the directory which the terminal is pointing out, and it moves around during the process.

[Kevin Buzzard]

In fact it seems to me that if those commands above work when your terminal is in the /Users/timchiu/repos/lean directory then you're all set. By the way, "work" means "returns no output". If you get an error then post it here.

[Tim Chiu]

Thank you so much! It's all working now.

[Qiye Tan]

It seems that I could not build elan in 2021 M1 Macbook.

image.png
image.png

It seems that there is something wrong with the linking process?
Any help is appreciated

[Patrick Stevens]

Qiye Tan said:

It seems that I could not build elan in 2021 M1 Macbook.

(As a general rule, it's always better to provide plain text rather than, or as well as, screenshots - someone who is debugging the problem may very well want to copy-paste some of the output.)

[Qiye Tan]

Thx~ I think it is caused by curl-rust (libcurl bindings for Rust).

[boris]

EDIT: Same issue as @Qiye Tan above.
Unfortunately, the elan installation is not working for me.
Proceeding without elan and seeing how far it gets me.

I'm on a 2021 M1 Macbook OS12.0.1
The error I'm getting after git checkout v1.0.7 && cargo buildis the following. I tried with a couple later version as well with no luck.

error: linking with `cc` failed: exit status: 1
  |
  = note: "cc" "-arch" "arm64"
...
[lots of lines of stuff]
...
 = note: ld: reference to symbol (which has not been assigned an address) __ZN4curl4init9INIT_CTOR17h0f90fe9ed6126500E in '__ZN4curl4init17h5336e02b4d062249E' from /Users/boris/repos/elan/target/debug/deps/libcurl-40c3b5b867aaff40.rlib(curl-40c3b5b867aaff40.curl.1df23e43-cgu.2.rcgu.o) for architecture arm64
          clang: error: linker command failed with exit code 1 (use -v to see invocation)```

[Sebastian Ullrich]

For what it's worth, installing elan the usual way Just Worked for me after choosing the correct shell

curl https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh -sSf | arch -x86_64 sh

[Julian Berman]

You have a different arch though right? They appear to have been building native ARM binaries.

[boris]

Sebastian Ullrich said:

For what it's worth, installing elan the usual way Just Worked for me after choosing the correct shell

curl https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh -sSf | arch -x86_64 sh

This works. However, one has to install Homebrew this way too. To check that you are using the right install of Homebrew you can do

% which brew
/usr/local/bin/brew

If you see

% which brew
/opt/homebrew/bin/brew

you are pointing to the wrong Homebrew.

In fact, it appears to be common to have 2 Homebrew versions or even just preferring the arch -x86_64 version.
I've opted for the approach of having an "Open with Rosetta" duplicate version of iTerm. See google for more, e.g. this or this.

I recommend this approach to new M1 Mac installers as general installation instructions apply once you run everything with Rosetta.

[Fedor Pavutnitskiy]

Thanks Sebastian and boris, just finished setting up lean 3 on the fresh macbook M1 using this approach and it works great. Here are the steps I've used:

1. open new terminal window and install xcode command line tools and rosetta 2 using xcode-select --install and softwareupdate --install-rosetta.

2. switch to the x86 architechture in the current terminal window by arch -x86_64 zsh as boris suggests. Everything below should happen in the same window.

3. install brew with /bin/bash -c "$(curl -fsSL https://raw.githubusercontent.com/Homebrew/install/HEAD/install.sh)"

4. the same steps as described in controlled installation for macos:

brew install elan mathlibtools
elan toolchain install stable
elan default stable

5. use leanproject get to get the repositories needed.

6. after that I've installed vs-code from the website and set it up as usual.

Looks like leanproject should always be called from arch -x86_64. Also I have no idea about performance downsides of using lean under rosetta vs natively.

[Sebastian Monnet]

@Trevor Fancher I followed your instructions and they worked - thank you very much. After having played around with the formalising-mathematics project, I decided to try the tutorials project using "leanproject get tutorials". This gave me the same error as in your guide (when you tried to get formalising-mathematics), but with 3.35.1 instead of 3.24.0, so I tried using the same solution, replacing 3.24.0 with 3.35.1, but this didn't work. As a workaround, I've just copied the contents of the lean files into the formalising-mathematics project, which seems to work, but obviously that's not a great fix. Do you have any idea what might have gone wrong?

[Kevin Buzzard]

This really stinks. I'm seeing undergraduates with "congratulations on getting to university here's a new Mac" laptops and they're having the same sort of problem too.

[Leon2k2k2k]

Hi new here, I am having the same problem: I can download everything but terminal can't find lean project...

[Leon2k2k2k]

never mind haha, I tried to install everything again and it works now!

[Bolton Bailey]

Following Fedor's instructions after trying to follow the instructions at the top of the page and failing to build elan like others. After installing homebrew again in the new architecture /usr/local/bin/brew now exists, but which brew still points to /opt/homebrew/bin/brew

[Bolton Bailey]

If it is indeed important to use the right brew here, it might be nice for Trevor to update the top comment again, or for Fedor's comment to specify the full path to the correct brew in its instructions.

[Kevin Buzzard]

I would urge people to update the community website rather than random zulip posts. People getting stuck trying to install Lean 3 on one of these cursed new macs is becoming a weekly occurrence amongst Imperial people.

[Kevin Buzzard]

"I want to get involved" -- "great, install lean by following the instructions on the community website to the letter" -- "but I have a new mac and I need help" -- [I now have to stop what I'm doing which is typically teaching someone how to use Lean at Xena or on the discord]

[Bolton Bailey]

Let me just confirm Fedor's instructions work, then I'll make a PR to update the site

[Kevin Buzzard]

Thank you so much. I wish I could help (because this is a pain point for me) but I don't have access to a new Mac, so all I do is moan :-(

[Bolton Bailey]

Hehe, I am using my mom's, she has one and I don't and I wanted to try lean out on it!

[Kevin Buzzard]

An MSc student who is fully signed-up to do her MSc project with me starting in January needs help with this, and now we've moved back to online so I can't even take her mac off her and throw it in the trash help her to install Lean on it

[Bolton Bailey]

Hmm, I can actually still call leanproject, even after restarting the terminal window, without rerunning the architecture change. Nevertheless, Fedor's instructions work, and I can use lean from VSCode. Worryingly, when trying to build mathlib from scratch using lean --make src, I did run into memory issues.

[Kevin Buzzard]

Do you have to build mathlib from scratch??

[Kevin Buzzard]

Why can't you use leanproject to download the oleans? Anyone would have memory issues if they tried to build mathlib from scratch nowadays. On one of my computers building mathlib from scratch reliably freezes it.

[Bolton Bailey]

No I don't have to build it from scratch - let me be clear. I just wanted to see if the M1 is as fast as they say by building mathlib on it.

[Bolton Bailey]

leanproject get-m works fine with this installation process, so it should be perfectly possible to use mathlib without building it. Perhaps you're right - it seems like building mathlib takes a lot of memory even on my intel Mac.

[Kevin Buzzard]

You can use flags such as -M6000 if building on the command line

[Bolton Bailey]

Ah, I see that command will cut down the memory usage. Thanks!

[Bolton Bailey]

Pull Request

[Kevin Buzzard]

Thank you so much!

[Eric Rodriguez]

Okay, so some updates - I just tried this on a new MBP (Lean took 5"14 to build here, which isn't too bad!) and I can confirm that the new instructions work for an Intel build. I seem to also be able to build from source and follow the build instructions from the top on that step, but Activity Monitor still reports it as an Intel arch build - I'll look into this tomorrow. And finally, most importantly as it relates to the comments on the PR, I installed all other components with the M1 homebrew, and it worked fine.

[Julian Berman]

I seem to also be able to build from source and follow the build instructions from the top on that step, but Activity Monitor still reports it as an Intel arch build

If you share what you ran happy to help with this -- just to be sure, you didn't run it from within the arch -x86_64 zsh shell hopefully? Otherwise what I run is rm -rf build; mkdir -p build/release; cd build/release; cmake -DCMAKE_PREFIX_PATH=/opt/homebrew/ -DCMAKE_INSTALL_PREFIX=/Users/julian/.local/share/lean/lean-"$(git name-rev HEAD --tags | sed 's;.*/v;;')"-darwin/ ../../src && make -j4 -- as long as you're not in an x86 shell that should work (or also don't set ARCHPREFERENCES=x84, etc)

[Julian Berman]

You can confirm you get an ARM build out of that from running file shell/lean, which should say it's an ARM executable if everything went well.

[Julian Berman]

Perhaps we should split the Zulip thread though for those stubborn enough to want ARM builds, I think there's already enough confusion on the above (and the PR is likely ready to merge so I'll put my token LGTM on it)

[Anne Baanen]

I went ahead and merged the instructions. Thank you all very much for writing and trying them out :heart:

[Eric Rodriguez]

ahh, I see what happened - I copied the wrong Lean installation over (I copied to stable, instead of leanprover-community-lean-3.35.1). I may make a little script that does this all correctly for me automatically, and learn some shell scripting for proper

[Julian Berman]

If you want to automate this more I'd instead recommend writing yourself a homebrew formula personally (one you use with your ARM brew). I have one for Lean 4 but I haven't cared enough to do so for Lean 3. Happy to share one too.

[Eric Rodriguez]

mind sharing it? it's probably helpful to others and can base the lean3 one off it sort of (although I guess it'll be quite different with lake and all)

[Julian Berman]

Sure. It's here: https://github.com/Julian/homebrew-tap/blob/master/Formula/lean%404.rb

[Julian Berman]

(And it's essentially directly copied from the upstream lean formula)

[Julian Berman]

A lean 3 one would be the same, the build process doesn't care much about lake

[Julian Berman]

(Keep in mind you'd need one of these for each Lean 3 version you want obviously, which is why people like elan fully handling the install)

[Eric Rodriguez]

can't you make it take an argument with the version? my idea was, if you run it in the directory with the lean installation, elan which lean gives you the right lean version, then you can make your lean locally and copy it into the right place

[Eric Rodriguez]

also tbf, it's only a minor inconvenience right now, as rosetta seems to be able to deal with lean these days just fine

[Julian Berman]

if you made the version be an argument homebrew won't let you install multiple separate invocations

[Julian Berman]

yes, I'd say if you're happy with rosetta I would not bother personally

[Julian Berman]

the only reason I do so is because I don't have or want an x86 homebrew install for any other reason

[Eric Rodriguez]

ahh, I see; don't really understand how homebrew works (still my first rodeo in OSX)

[Julian Berman]

don't worry no one does :P (let alone me)

[Eric Rodriguez]

OK, cool, so I've got this little shell script now:

#!/bin/zsh

set -x

version="v"
if [[ $(elan which lean) =~ "leanprover-community--lean---(.*)\/bin\/lean$" ]] then
  version+=$match
fi

if [[ version == "v" ]] then
  echo "elan which lean reported an unsupported Lean path:"
  echo $(elan which lean)
  exit 1
fi

lenloc=$(elan which lean)
chkloc=$(elan which leanchecker)
pkgloc=$(elan which leanpkg)

# Set this to a local clone of leanprover-community/lean (that you don't mind being messed with!)
cd ~/repos/lean
# Note that this is very destructive!!!
git clean -fdx
git switch master
git pull
git checkout $version
mkdir -p build/release
cd build/release
cmake -DCMAKE_PREFIX_PATH=/opt/homebrew/ -DCMAKE_INSTALL_PREFIX=~/repos/lean/ ../../src
make bin_lean  -j10
cd ../../
cp bin/lean $lenloc
cp bin/leanpkg $pkgloc
cp build/release/checker/leanchecker $chkloc

I'd really appreciate if people could try this and tell me how well it works; the idea is that after you leanproject get some repo, and elan installs the x86 version of leanprover-community lean required to run it, this replaces the relevant binaries with the ARM version (i.e. the workflow I use is leanproject get mathlib; cd mathlib; this_script)

Firstly, wow Lean builds in a minute - my poor 3600X was taking like 4 minutes with -j12...

Secondly, this is actually not perfect; I don't know the right make target that will make just lean, leanpkg and leanchecker. If you just leave it on default, it'll build all of the stdlib for no real reason; but bin_lean doesn't make leanchecker; please let me know if anyone knows!

And also, lastly, currently this script seems to need sudo to copy the files at the end? Which isn't great... I feel like I got wrong permissions somewhere, but this is my first time using a Unix-like OS. If someone can tell me how I can fix that, that'd be much appreciated.

[Eric Rodriguez]

Ahh, I see the permissions issue. elan downloads lean(pkg|checker)? as r-xr-xr-x, so I can't cp on top of them. my current idea for a workaround (as we should own these files) are chmod u+w lean, cp blah, chmod u-w lean; is there a better way to do that?

[Eric Rodriguez]

anyways, I can finally get to maths, which is the happy thing :D

[Sebastian Monnet]

I followed @Fedor Pavutnitskiy's instructions and have it now semi-working. I've been able to use leanproject get tutorials and leanproject get ImperialCollegeLondon/formalising-mathematics and have both projects working successful. However, when I try to run leanproject new test_project I get a very long error that ends with Command '['leanpkg', 'new', 'test_project']' returned non-zero exit status 1.. I have tried restarting my computer and it hasn't made any difference.

[Sebastian Monnet]

Does anyone know how I can fix this?

[Kevin Buzzard]

Can you post the error? Do you have write access to the directory where you ran the command?

[Sebastian Monnet]

Sadly the error is over a million characters, and Zulip only lets me post ten thousand

[Sebastian Monnet]

I'm pretty sure I do have access

[Sebastian Monnet]

Here are the first few lines of the error

/Users/sebastianmonnet/.elan/toolchains/stable/lib/lean/library/init/data/option/basic.lean:30:41: error: type expected at
  o.is_some
term has type
  bool
/Users/sebastianmonnet/.elan/toolchains/stable/lib/lean/library/init/data/option/basic.lean:30:41: error: type expected at
  o.is_some
term has type
  bool
/Users/sebastianmonnet/.elan/toolchains/stable/lib/lean/library/init/meta/expr.lean:149:14: error: failed to synthesize instance name, name should be provided explicitly
/Users/sebastianmonnet/.elan/toolchains/stable/lib/lean/library/init/meta/expr.lean:322:28: error: function expected at
  f
term has type
  expr
/Users/sebastianmonnet/.elan/toolchains/stable/lib/lean/library/init/meta/expr.lean:353:23: error: function expected at
  e
term has type
  expr
/Users/sebastianmonnet/.elan/toolchains/stable/lib/lean/library/init/meta/local_context.lean:2:0: warning: imported file '/Users/sebastianmonnet/.elan/toolchains/stable/lib/lean/library/init/meta/expr.lean' uses sorry
/Users/sebastianmonnet/.elan/toolchains/stable/lib/lean/library/init/meta/pexpr.lean:7:0: warning: imported file '/Users/sebastianmonnet/.elan/toolchains/stable/lib/lean/library/init/meta/expr.lean' uses sorry
/Users/sebastianmonnet/.elan/toolchains/stable/lib/lean/library/init/meta/has_reflect.lean:7:0: warning: imported file '/Users/sebastianmonnet/.elan/toolchains/stable/lib/lean/library/init/meta/expr.lean' uses sorry
/Users/sebastianmonnet/.elan/toolchains/stable/lib/lean/library/init/meta/expr_address.lean:11:0: warning: imported file '/Users/sebastianmonnet/.elan/toolchains/stable/lib/lean/library/init/meta/expr.lean' uses sorry
/Users/sebastianmonnet/.elan/toolchains/stable/lib/lean/library/init/meta/declaration.lean:7:0: warning: imported file '/Users/sebastianmonnet/.elan/toolchains/stable/lib/lean/library/init/meta/expr.lean' uses sorry
/Users/sebastianmonnet/.elan/toolchains/stable/lib/lean/library/init/meta/expr_address.lean:11:0: warning: imported file '/Users/sebastianmonnet/.elan/toolchains/stable/lib/lean/library/init/data/option/basic.lean' uses sorry
/Users/sebastianmonnet/.elan/toolchains/stable/lib/lean/library/init/meta/local_context.lean:2:0: warning: imported file '/Users/sebastianmonnet/.elan/toolchains/stable/lib/lean/library/init/data/option/basic.lean' uses sorry
/Users/sebastianmonnet/.elan/toolchains/stable/lib/lean/library/init/meta/environment.lean:8:0: warning: imported file '/Users/sebastianmonnet/.elan/toolchains/stable/lib/lean/library/init/data/option/basic.lean' uses sorry
/Users/sebastianmonnet/.elan/toolchains/stable/lib/lean/library/init/meta/interaction_monad.lean:10:0: warning: imported file '/Users/sebastianmonnet/.elan/toolchains/stable/lib/lean/library/init/data/option/basic.lean' uses sorry
/Users/sebastianmonnet/.elan/toolchains/stable/lib/lean/library/init/meta/interaction_monad.lean:10:0: warning: imported file '/Users/sebastianmonnet/.elan/toolchains/stable/lib/lean/library/init/meta/expr.lean' uses sorry
/Users/sebastianmonnet/.elan/toolchains/stable/lib/lean/library/init/meta/tactic.lean:11:0: warning: imported file '/Users/sebastianmonnet/.elan/toolchains/stable/lib/lean/library/init/data/option/basic.lean' uses sorry
/Users/sebastianmonnet/.elan/toolchains/stable/lib/lean/library/init/meta/tactic.lean:11:0: warning: imported file '/Users/sebastianmonnet/.elan/toolchains/stable/lib/lean/library/init/meta/expr.lean' uses sorry
/Users/sebastianmonnet/.elan/toolchains/stable/lib/lean/library/init/meta/tactic.lean:1578:10: error: function expected at
  expr.const (name.mk_string "dite" name.anonymous) [tgt_u]
term has type

[Kevin Buzzard]

Oh you've posted enough! What does elan show print out? Maybe elan default leanprover-community-lean-3.30.0 will help? I doubt it will do much harm. I'm wondering if your default lean toolchain is lean 4.

[Sebastian Monnet]

elan show prints out

installed toolchains
--------------------

stable (default)
leanprover-community/lean:3.24.0
leanprover-community/lean:3.35.1

active toolchain
----------------

stable (default)
Lean (version 3.33.0, commit a0fb1e8c7ac8, Release)

[Sebastian Monnet]

So I guess it's not that?

[Eric Rodriguez]

can you try get the first few lines of the errors?

[Sebastian Monnet]

Eric Rodriguez said:

can you try get the first few lines of the errors?

What do you mean? Is that not what I posted above?

[Eric Rodriguez]

this looks like the sort of errors I get when Lean didn't want to compile properly when you're compiling from source, but Fedor's instructions don't seem to

[Eric Rodriguez]

Sebastian Monnet said:

Eric Rodriguez said:

can you try get the first few lines of the errors?

What do you mean? Is that not what I posted above?

oh, what?! that's almost weirder...

[Eric Rodriguez]

what arch terminal are you running leanproject from?

[Sebastian Monnet]

I've tried both the default and the x86 one from Fedor's instructions

[Eric Rodriguez]

can you post a full shell-log on something like pastebin or gists

[Sebastian Monnet]

https://gist.github.com/SebastianMonnet/a2d6531bfc7e588d3e928f84a4e851d5

[Eric Rodriguez]

can you try setting the elan default to a lean install that you've used in some other context, e.g. 3.35.1?

[Eric Rodriguez]

i'm not too sure what's going on but my first idea is that leanpkg is written in lean itself, so that may have something to do with it

[Sebastian Monnet]

Okay I just did this

[Sebastian Monnet]

Will try making a leanproject

[Sebastian Monnet]

ooh

[Sebastian Monnet]

It's doing something different now!

[Sebastian Monnet]

Seems to be working

[Sebastian Monnet]

Will report back once it's done

[Kevin Buzzard]

another bruised and battered user struggles to the top of the "installing Lean 3 on an M1" mountain

[Kevin Buzzard]

Do we need to add some comments about setting default elan toolchain? I am a bit confused about why this is happening -- changing my default toolchain between lean 3 versions shouldn't break leanproject right?

[Sebastian Monnet]

Yes the project works

[Eric Rodriguez]

I think the oleans or something is broken, I personally haven't tried stable so i'm going to run some tests to see what's going on

[Sebastian Monnet]

Thank you both for your help

[Kevin Buzzard]

For me the only thing which changes if I change my default toolchain is that at the very beginning of the output with leanproject new I get a different default branch (which is deleted later on):

$ leanproject new test1
> cd test1
> git init -q
> git checkout -b lean-3.33.0
Switched to a new branch 'lean-3.33.0'
configuring test1 0.1
Adding mathlib
mathlib: cloning https://github.com/leanprover-community/mathlib to _target/deps/mathlib
...

As far as I know that 3.33 stuff (which is irrelevant) is the only thing affected by the default toolchain

[Eric Rodriguez]

leanpkg is run on lean itself, it's not a python program or anything so if that Lean install is borked then it will blow up

[Kevin Buzzard]

Note that mathlib master is on 3.35.1 right now and the project works fine, it's just that one random bit at the beginning; that's the only way you can tell what your default toolchain is in the process.

[Kevin Buzzard]

Oh so you're suggesting that Sebastian has a borked 3.33 install?

[Kevin Buzzard]

Not that this matters much any more

[Eric Rodriguez]

that's my only idea so far, yeah, or the 3.33 install doesn't work on M1 for some reason; something'sdefinitely weird because I just reinstalled stable on my elan and it came as 3.35.1

[Eric Rodriguez]

Eric Rodriguez said:

OK, cool, so I've got this little shell script now:

#!/bin/zsh

set -x

version="v"
if [[ $(elan which lean) =~ "leanprover-community--lean---(.*)\/bin\/lean$" ]] then
  version+=$match
fi

if [[ version == "v" ]] then
  echo "elan which lean reported an unsupported Lean path:"
  echo $(elan which lean)
  exit 1
fi

lenloc=$(elan which lean)
chkloc=$(elan which leanchecker)
pkgloc=$(elan which leanpkg)

# Set this to a local clone of leanprover-community/lean (that you don't mind being messed with!)
cd ~/repos/lean
# Note that this is very destructive!!!
git clean -fdx
git switch master
git pull
git checkout $version
mkdir -p build/release
cd build/release
cmake -DCMAKE_PREFIX_PATH=/opt/homebrew/ -DCMAKE_INSTALL_PREFIX=~/repos/lean/ ../../src
make -j10
cd ../../
chmod u+w $lenloc $pkgloc $chkloc
cp bin/lean $lenloc
cp bin/leanpkg $pkgloc
cp build/release/checker/leanchecker $chkloc
chmod u-w $lenloc $pkgloc $chkloc

I'd really appreciate if people could try this and tell me how well it works; the idea is that after you leanproject get some repo, and elan installs the x86 version of leanprover-community lean required to run it, this replaces the relevant binaries with the ARM version (i.e. the workflow I use is leanproject get mathlib; cd mathlib; this_script)

Firstly, wow Lean builds in a minute - my poor 3600X was taking like 4 minutes with -j12...

Secondly, this is actually not perfect; I don't know the right make target that will make just lean, leanpkg and leanchecker. If you just leave it on default, it'll build all of the stdlib for no real reason; but bin_lean doesn't make leanchecker; please let me know if anyone knows!

~~And also, lastly, currently this script seems to need sudo to copy the files at the end? Which isn't great... I feel like I got wrong permissions somewhere, but this is my first time using a Unix-like OS. If someone can tell me how I can fix that, that'd be much appreciated.~ ~ see below

I've updated to one that shouldn't run into permission issues - if someone knows a better way to write the shell script lmk! Would also appreciate someone else testing it to see if it's worth using.

[Louis Theran]

I was a little worried that the solutions above were beyond my competence, since I don't really understand how lean installs itself. As an alternative, which might be better for beginners, I used Docker and the dev container setup from https://github.com/danielbush/lean-remote-containers.

This more or less worked out of the box, presumably because the Docker images are Linux, which elan supports.

I did run into one problem, which is that, if you start with a "bare" directory, lean complains about not having a leanpkg.toml file. My rather unsightly solution was to run leanproject and then restart.

[Bryan Gin-ge Chen]

Welcome, Louis! Great to see you here!

[Bryan Gin-ge Chen]

I don't have an M1 mac so I haven't tested them but I think the current recommended instructions are here; did you try these / have any trouble with them? https://leanprover-community.github.io/install/macos.html#m1-macs--apple-silicon

[Louis Theran]

Bryan Gin-ge Chen said:

I don't have an M1 mac so I haven't tested them but I think the current recommended instructions are here; did you try these / have any trouble with them? https://leanprover-community.github.io/install/macos.html#m1-macs--apple-silicon

I didn't so far, since I got a little scared off by having to install a second homebrew for a different architecture.

Since just running in Docker works more or less perfectly, I didn't try anything else. (Though I can easily imagine a more refined version where one doesn't need devcontainers and just uses "docker run lean" as the executable.)