Installing mathlib on M1 Mac

Stream: lean4

[Dean Young]

After installing the mathlibtools, what is one supposed to do in order to use the library?

For example, this:

import data.array.lemmas

produces an error response:

file 'data/array/lemmas' not found in the search path
Use 'lean --path' to see where lean is looking, or https://leanprover-community.github.io/file-not-found.html for more

under lean --path, I get this:

{
  "is_user_leanpkg_path": true,
  "leanpkg_path_file": "/Users/edeany/.lean/leanpkg.path",
  "path": [
    "/Users/edeany/.elan/toolchains/stable/bin/../library",
    "/Users/edeany/.elan/toolchains/stable/bin/../lib/lean/library"
  ]
}

Which doesn't seem to include mathlibtools where data resides.

[Dean Young]

oh hold on I just saw the link - I'll go complete the steps there

[Kevin Buzzard]

If you're talking about mathlib then just to note that this is a lean 3 library and you're posting in the lean 4 stream

[Dean Young]

hold on ... i've got lean 4 ... does this mean I have to switch to lean 3 for the lib to work?

[Mauricio Collares]

Yes for the time being, since mathlib is still being ported to Lean 4. But if you created your project with leanproject new (I'm assuming you're working on a project which depends on mathlib and not on mathlib itself), then there should be a leanpkg.toml file at the project root which instructs the elan you already have to fetch and use a Lean 3 build.

[Mauricio Collares]

If your default elan toolchain is Lean 4, leanproject new might throw an error like error: toolchain 'leanprover/lean4:nightly' does not have the binary ".../.elan/toolchains/leanprover--lean4---nightly/bin/leanpkg". This is an unfortunate consequence of the fact that leanpkg no longer exists in Lean 4, but it only affects creating new projects and fetching them, not day-to-day use.

You can work around it by setting the default toolchain to Lean 3 by running elan default leanprover-community/lean:stable before running leanproject new. I don't know if there's a better workaround.

[Stavan Jain]

Hello, I'm having some trouble installing lean and mathlib on my Macbook Air with an M2 chip. I've been following these instructions: https://leanprover-community.github.io/install/macos.html

[Stavan Jain]

After completing step 4, I get this error message:
image.png

[Patrick Massot]

Please don't double-post, this won't help anything.

[Stavan Jain]

I apologize, I thought I posted in the wrong place, so i decided to post here as well

[Sebastian Ullrich]

You are posting in the lean4 channel, but the instructions you posted are for Lean 3

[Mauricio Collares]

@Stavan Jain Lean 3 does not have native M1 builds, you have to install brew under Rosetta (and run all installation commands inside the Rosetta shell).

That being said, are you sure you don't want Lean 4? It is not backwards compatible, but a significant portion of the mathematics library has already been ported to Lean 4 and the porting process should be finished in a few months. It is highly dependent on what your immediate use for Lean is. If you just want to explore, Lean 4 is a good option.

[rami3l]

I just added homebrew arm64 distribution for elan-init, so everything should be fine if you just run brew install elan-init and use the Lean 4 version pinned by mathlib4.

[rami3l]

Lean 3 will probably be deprecated in the near future when Lean 4 reaches parity.

[Julian Berman]

Did you check we have ARM64 builds being built? The reason I didn't add elan-init for ARM previously was because we did not previously, which is worse behavior, someone then can install elan but immediately gets errors when they try to install toolchains.

[Julian Berman]

Ah nice, it looks like there indeed are darwin_aarch64 builds in the lean4-nightly repo.

[Stavan Jain]

Thank you for the responses! My research group is using Lean 3 so needed to install that. Will suggest lean 4 though. Everything is working as it should now.