Zulip Chat Archive

Stream: lean4

Topic: Installing mathlib on M1 Mac


Dean Young (Sep 30 2022 at 23:38):

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 (Sep 30 2022 at 23:42):

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

Kevin Buzzard (Sep 30 2022 at 23:43):

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 (Sep 30 2022 at 23:49):

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

Mauricio Collares (Sep 30 2022 at 23:54):

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 (Sep 30 2022 at 23:57):

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 (May 22 2023 at 17:42):

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 (May 22 2023 at 17:43):

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

Patrick Massot (May 22 2023 at 17:43):

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

Stavan Jain (May 22 2023 at 17:45):

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

Sebastian Ullrich (May 22 2023 at 17:59):

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

Mauricio Collares (May 22 2023 at 19:28):

@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 (May 22 2023 at 23:31):

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 (May 22 2023 at 23:33):

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

Julian Berman (May 23 2023 at 13:46):

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 (May 23 2023 at 13:47):

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

Stavan Jain (May 24 2023 at 17:29):

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.


Last updated: Dec 20 2023 at 11:08 UTC