Zulip Chat Archive

Stream: new members

Topic: How do I increase the memory consumption limit?


view this post on Zulip Abhimanyu Pallavi Sudhir (Nov 11 2018 at 13:14):

I keep getting "excessive memory consumption" errors in Lean. How can I increase the memory consumption limit? Presumably this is a Lean setting, right?

view this post on Zulip Abhimanyu Pallavi Sudhir (Nov 11 2018 at 13:16):

From the docs for the extension, it's lean.memoryLimit or -M but I'm not sure how to use this.

view this post on Zulip Reid Barton (Nov 11 2018 at 13:18):

Have you built your project (e.g. with leanpkg build) recently? The most common reason for running into the memory consumption error is that you don't have up-to-date compiled versions of your dependencies, and so Lean has to do a lot more work every time it processes your file.

view this post on Zulip Reid Barton (Nov 11 2018 at 13:19):

You may need to restart the Lean server afterwards too

view this post on Zulip Kevin Buzzard (Nov 11 2018 at 13:21):

Yes -- increasing the memory is ironically probably not the way to solve these errors -- you have maybe got buggy code or you need to compile stuff

view this post on Zulip Kevin Buzzard (Nov 11 2018 at 13:22):

And whenever you get it you should restart lean I guess, eg with ctrl shift p lean: restart

view this post on Zulip Abhimanyu Pallavi Sudhir (Nov 11 2018 at 13:25):

Buggy code isn't the issue, since it works after restarting (albeit after a very long time). As for the installation -- I installed from the binaries you (@Kevin Buzzard) uploaded as of October. Is this too old?

view this post on Zulip Reid Barton (Nov 11 2018 at 13:26):

Are you working on mathlib, or your own project which uses mathlib, or something else?

view this post on Zulip Abhimanyu Pallavi Sudhir (Nov 11 2018 at 13:34):

A project which uses a local download of mathlib.

view this post on Zulip Kenny Lau (Nov 11 2018 at 13:40):

lean --make

view this post on Zulip Kenny Lau (Nov 11 2018 at 13:40):

or leanpkg build

view this post on Zulip Kevin Buzzard (Nov 11 2018 at 15:03):

If code takes a long time to run you can try and figure out what's going on by sticking #exit in the code and working out which line is causing the problem. October binaries are fine I'm sure. But there is perhaps a line which is bad style or could be rewritten to solve your problems


Last updated: May 16 2021 at 21:11 UTC