How do I increase the memory consumption limit?

Stream: new members

[Abhimanyu Pallavi Sudhir]

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

[Abhimanyu Pallavi Sudhir]

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

[Reid Barton]

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.

[Reid Barton]

You may need to restart the Lean server afterwards too

[Kevin Buzzard]

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

[Kevin Buzzard]

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

[Abhimanyu Pallavi Sudhir]

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?

[Reid Barton]

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

[Abhimanyu Pallavi Sudhir]

A project which uses a local download of mathlib.

[Kenny Lau]

lean --make

[Kenny Lau]

or leanpkg build

[Kevin Buzzard]

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