Mathlib and lean server consumes too much memory on mac m1

Stream: new members

[Hyunggyu Jang]

Hi, I’m newbie about lean and mathlib also. And I’m trying to set up mathlib facilities on my environment, mac m1. To do so, I’ve followed the instructions for quick start, that is, leanproject get tutorials. Launched 00_first_proofs.lean, and wait for a while for lean to correctly load the dependencies and compile.

It seemed to work for a while, but seems with some noticeable lags, and eventually spitted an error message saying

error: excessive memory consumption detected at ’replace’ (potential solution: increase memory consumption threshold)

To inspect what’s going on, first, I opened Activity Monitor, and confirmed lean itself consumes too much memory:
Screen-Shot-2021-05-06-at-12.03.19-PM.png

Thanks for all your hard work!

Best regards,
-- Hyunggyu Jang

[Bryan Gin-ge Chen]

Did you open the tutorials directory in VS Code, or just the file 00_first_proofs.lean?

[Hyunggyu Jang]

Thanks for your quick reply!

I’ve launched 00_first_proofs.lean at Emacs directly.

[Bryan Gin-ge Chen]

Oh, I see. I'm not sure if the same is true for the emacs mode, but at least for VS Code you have to open the directory, not just a single file.

[Hyunggyu Jang]

At least, to me, there’s no way to trigger lean server by opening the enclosing directory, not the file itself.

I really love Emacs, so I want to avoid to use VS Code.

Thanks!

[Bryan Gin-ge Chen]

If you navigate to your tutorials directory in the console and run ls _target/deps/mathlib/src/algebra do you see any files with a .olean extension? If so, that means that leanproject did at least get the compiled files which should make Lean load quickly.

[Hyunggyu Jang]

Yes, I can confirm it compiled to *.olean along with its source file, *.lean

[Hyunggyu Jang]

Furthermore, even after I met such an error from lean server, I still can interact as normal. The only problem seems to be the fact that I consumes too much memory. It affects my OS’s behavior noticeably.

[Bryan Gin-ge Chen]

Well, the reason Lean is using so many resources is because it's recompiling the .lean files. What version of Lean are you using?

[Bryan Gin-ge Chen]

We don't have an official M1 release, so just to be sure, are you using the x86 version coming from elan?

[Hyunggyu Jang]

The latest one, 3.30c. But it seems like the tutorial wants 3.28 version.

Oh, elan seems to have gmp path problem, and even I set it properly by

install_name_tool -change /usr/local/opt/gmp/lib/libgmp.10.dylib /opt/homebrew/lib/libgmp.10.dylib ~/.elan/toolchains/leanprover-community--lean---3.28.0/bin/lean

As my gmp is arm64 version, it conflicted with lean executable.

So I’ve gone with brew’s lean, which supports arm64 architecture, plus, it supports HEAD option, which presumably builds lean from github repository, I guess.

[Hyunggyu Jang]

Since lean doesn’t support m1 officially, then maybe I should use Rosetta 2 for emulating intel architecture?

[Bryan Gin-ge Chen]

Yes, I think Rosetta + elan is still the recommended way to go.

We don't recommend using homebrew, as that only installs a single version of Lean and you may find yourself looking at projects which require different versions of Lean, e.g. the tutorials which are on 3.28 and mathlib which is currently on 3.30.

[Bryan Gin-ge Chen]

I think @Julian Berman has been using Lean on an M1 Mac; he might have some more advice.

[Hyunggyu Jang]

Thanks for redirecting! I hope I can get some insight how to setup lean in M1.

For the Rosetta + elan combination, I guess should install Rosetta version homebrew.

Thanks for your sincere advice! At least, I think, I found what caused the excessive memory consumption from lean server side!

[Hyunggyu Jang]

For anyone who reached this discussion, if one scarifies version managing facilities from elan, that is, if you are okay with a single version of lean, you can do it as following, at least for the tutorials:

1. Install the latest lean via either from source or homebrew. For example, I’ve installed with the command:

brew install lean --HEAD

At the time of writing, it should match with the version supported by `mathlib`.

2. Build tutorials with leanpackage get tutorials. It is for getting the source files from tutorials rather than building mathlib dependencies, which are to be done via the following step.
3. Build mathlib dependency with leanpackage new. Note that this should be issued other than the tutorials directory to avoid meta configuration file conflicts. You shouldn’t get any error messages in this step.
4. Move the source codes from tutorials to the newly built project. Might need to adjust leanpkg.toml or leanpkg.path.

Result?
Screen-Shot-2021-05-06-at-1.36.17-PM.png

All I needed was to taste and experiment with lean, thus, felt a single version of lean is more than sufficient to me.
Thanks for guiding me, @Bryan Gin-ge Chen!!

[Brandon Brown]

I'm getting the same error in VS Code on Macbook Air M1 with 16GB RAM: "excessive memory consumption detected at 'replace' (potential solution: increase memory consumption threshold)" only when importing from mathlib it seems.

[Kevin Buzzard]

Do you have a fully compiled mathlib on your system? If not then that error is not unexpected

[Brandon Brown]

I fixed it somehow. I had the folder syncing with Dropbox, so I disabled that in case dropbox was messing with things. I also deleting the project and all the files and then did a fresh leanproject new and now it's so far not giving me that error.

[Scott Viteri]

Switching back to lean3 from lean4, I am having the same issue with Emacs getting up an running:
Lean (version 3.30.0, commit a5822ea47ebc, Release)
Used leanproject to get mathlib, where I have oleans
mathlib = {git = "https://github.com/leanprover-community/mathlib", rev = "ea0043ca0f7c83de3103c0a5b87b7b39717cb837"}
VSCode runs import topology.basic without issues, and an otherwise responsive Emacs lean-mode will spin up several threads and hang. Looks like it may be unable to find/use the oleans, and is trying to rebuild mathlib.