installing lean3+mathlib on M1 mac

Stream: new members

[Laurent Bartholdi]

Hi all! I also have an M1 mac now, and am stuck :( can any kind soul help?

Installation of lean, leanproject etc. went well, I have the native versions from homebrew and followed the trick to install leanpkg (without actually creating a parallel x86-homebrew).

I can then run "leanproject new testproject", which gives me a fresh project with lean 3.50.3

I can then "cd testproject" and "emacs src/test.lean" and type "#check 1" which works well.

However, I type "import algebra.group.basic" and all hell breaks loose: "invalid import data.option.defs", "excessive memory consumption" etc.

[Anne Baanen]

This suggests Mathlib hasn't been successfully added to your project. What happens after running leanproject add-mathlib in your project folder and trying again to import algebra.group.basic?

[Laurent Bartholdi]

Thanks Anne, you're a magician!
It said "This project already depends on mathlib"; but now all works!

[Laurent Bartholdi]

Uh... celebrated too quickly. import algebra.group.basic works, but import tactic produces

invalid import: data.option.defs
excessive memory consumption detected at 'expression traversal' (potential solution: increase memory consumption threshold)
invalid import: data.option.defs
invalid object declaration, environment already has an object named 'option.elim._main'
invalid import: data.option.defs
invalid object declaration, environment already has an object named 'option.elim._main'
invalid import: data.option.defs
invalid object declaration, environment already has an object named 'option.elim._main'
invalid import: data.option.defs
invalid object declaration, environment already has an object named 'option.elim._main'
invalid import: data.quot
excessive memory consumption detected at 'replace' (potential solution: increase memory consumption threshold)
invalid import: algebra.group.defs
excessive memory consumption detected at 'expression traversal' (potential solution: increase memory consumption threshold)
invalid import: algebra.group.defs
invalid object declaration, environment already has an object named 'has_vadd'
invalid import: data.prod.basic
excessive memory consumption detected at 'replace' (potential solution: increase memory consumption threshold)
invalid import: algebra.group.defs
invalid object declaration, environment already has an object named 'has_vadd'
invalid import: order.hom.basic
excessive memory consumption detected at 'expression traversal' (potential solution: increase memory consumption threshold)
invalid import: algebra.group.defs
invalid object declaration, environment already has an object named 'has_vadd'
invalid import: data.prod.basic
invalid object declaration, environment already has an object named 'prod_map'
invalid import: order.rel_classes
excessive memory consumption detected at 'replace' (potential solution: increase memory consumption threshold)
invalid import: order.lattice
excessive memory consumption detected at 'replace' (potential solution: increase memory consumption threshold)
invalid import: order.lattice
invalid object declaration, environment already has an object named 'le_antisymm''
invalid import: order.lattice
invalid object declaration, environment already has an object named 'le_antisymm''
invalid import: order.with_bot
excessive memory consumption detected at 'expression traversal' (potential solution: increase memory consumption threshold)
invalid import: algebra.group.defs
invalid object declaration, environment already has an object named 'has_vadd'
...

How can I determine which parts of my install are broken? It used to work just fine^{TM} before that.

[Ruben Van de Velde]

I'd first try to close vs code and start again - if that doesn't work, probably your cache is messed up

[Laurent Bartholdi]

@Ruben Van de Velde yes, I'm sure my cache is messed up! Just, how do I unmess it? I use emacs. I tried leanproject get-mathlib-cache and leanproject add-mathlib. Also, leanproject check say's I'm good.

[Anne Baanen]

If you already ran leanproject get-mathlib-cache without issues, then running lean --make _target/deps/mathlib/src/tactic/default.lean in your project directory should finish within a few seconds with no output.

[Anne Baanen]

If this takes a long time and/or gives output, I'd delete the cache (~/.mathlib/bunch-of-numbers.tar.xz) and rerun leanproject get-mathlib-cache.

[Anne Baanen]

If the lean command finishes quickly, then the issue is probably with Emacs. On VS Code or nvim I'd advise making sure to run your editor in the right working directory (i.e. Open Folder in the menu or :cd ...), but I recall that (spac)emacs, back when I used to use it, already automatically opened the right directory. Still, something you might want to try out.

[Laurent Bartholdi]

@Anne Baanen I tried this; this is what happens:

% rm ~/.mathlib/*xz
% leanproject get-mathlib-cache
Looking for mathlib oleans for 6890b009ba
  locally...
  remotely...
  Found remote mathlib oleans
Located matching cache
  6890b009ba: 100%|█████████████████████████████████████████████████████████████████| 84.6M/84.6M [00:13<00:00, 6.40MB/s]
Applying cache
  files extracted: 3036 [00:05, 603.78/s]
% lean --make _target/deps/mathlib/src/tactic/default.lean
/Users/laurent/src/lean/testproject/_target/deps/mathlib/src/logic/function/basic.lean: function.factors_through.apply_ex/Users/laurent/src/lean/testproject/_target/deps/mathlib/src/logic/relation.lean: relation.refl_trans_gen.head_induction_/Users/laurent/src/lean/testproject/_target/deps/mathlib/src/logic/relation.lean: relation.refl_trans_gen.total_of_right_/Users/laurent/src/lean/testproject/_target/deps/mathlib/src/order/monotone/basic.lean: not_monotone_not_antitone_iff_exi/Users/laurent/src/lean/testproject/_target/deps/mathlib/src/logic/equiv/basic.lean: equiv.prod_congr_left_trans_prod_com/Users/laurent/src/lean/testproject/_target/deps/mathlib/src/control/traversable/lemmas.lean: traversable.traverse_eq_map/Users/laurent/src/lean/testproject/_target/deps/mathlib/src/logic/equiv/basic.lean: parsing at line 1312^C

(I interrupted it when it was clear it was recompiling everything).

[Anne Baanen]

Perhaps the lean versions mismatch? What is the output of lean --version, the value of lean_version in leanpkg.toml and the value of lean_version in _target/deps/mathlib/leanpkg.toml? If they mismatch, try changing the value in leanpkg.toml to match that one in _target/deps/mathlib/leanpkg.toml and recompiling.

[Laurent Bartholdi]

% lean --version
Lean (version 3.50.3, Release)
% grep lean_version _target/deps/mathlib/leanpkg.toml leanpkg.toml
_target/deps/mathlib/leanpkg.toml:lean_version = "leanprover-community/lean:3.50.3"
leanpkg.toml:lean_version = "leanprover-community/lean:3.50.3"
% which lean
/opt/homebrew/bin/lean

[Anne Baanen]

It's somewhat suspicious that which lean returns a path in homebrew, shouldn't it be something like ~/.elan/bin/lean? But the version numbers look okay so that is probably not it...

[Anne Baanen]

I think we'll need someone with actual Mac (M1) experience to take a look at this :(

[Alistair Tucker]

What is the "leanpkg trick"?

[Laurent Bartholdi]

@Alistair Tucker The "leanpkg trick" is to install leanpkg, and then modify its x86_64 executables by hand to make them point to native ones.

@Anne Baanen It's stranger and stranger... after a few random attempts (which I didn't write down) I got at one moment the lean --make command to return without output. I can't get there anymore now; however, it seems that just letting lean --make run recomputes the cache, and I'm now in a state where I can work. This is perfectly acceptable for me; is there a command such as leanproject compile-mathlib which would run all the necessarylean --make for me, without attempting to pull a cache?

[Alistair Tucker]

It's not clear how it might cause the problems you describe, but your setup is distinctly nonstandard. Still it sounds like someone got it working at some point and left instructions that you were able to follow? You should be able to achieve something similar using elan (which virtually everyone does) and in particular elan toolchain link.

[Julian Berman]

I only skimmed the thread, so possibly someone's mentioned it, but yeah, having an /opt/homebrew/bin/lean means you ran brew install lean at some point, so run brew uninstall lean. Depending on where you have put the elan toolchain directory on your PATH that may be your only issue, or you may still have another.

[Julian Berman]

So run the brew uninstall then share type -a lean probably

[Alistair Tucker]

Well Laurent will still need a lean and last time I checked elan was not able to find an aarch_64 version by itself. My idea was rather that elan toolchain link be used to link to the lean in opts/homebrew. I can't claim to have tried exactly that, but I have used elan to link to an aarch_64 lean compiled locally (which remains yet another option).

[Laurent Bartholdi]

OK, a progress report. My idea was to install elan as a x86_64 application, and then elan toolchain link the homebrew version of lean into elan. It seems that only using the self-compiled lean works, though, something must be weird with homebrew's. Here's in summary what I did, hopefully it helps someone in the same situation as mine.

cd /usr/local/src
git clone https://github.com/leanprover/elan.git
git clone https://github.com/leanprover/lean.git
cd elan
cargo build && cargo install
cd target/release
./elan-init
# don't panic about error messages which will come up when elan fails to find binaries!
# each time you see a missing binary, carefully note its release number and follow steps such as the following.
cd /usr/local/src/lean
git checkout v3.24.0 && mkdir -p build/release && cd build/release
cmake -DCMAKE_INSTALL_PREFIX=/usr/local/src/lean/v3.24.0 ../../src && make -j install
elan toolchain link leanprover-community--lean---3.24.0 /usr/local/src/lean/v3.24.0

cd /usr/local/src/lean
git checkout v3.50.3 && mkdir -p build/release && cd build/release
cmake -DCMAKE_INSTALL_PREFIX=/usr/local/src/lean/v3.50.3 ../../src && make -j install
elan toolchain link leanprover-community--lean---3.50.3 /usr/local/src/lean/v3.50.3

elan toolchain link stable /usr/local/src/lean/v3.50.3
elan default stable

[Alistair Tucker]

In fact elan also has an aarch_64 version that you can install using the instructions here.