Zulip Chat Archive

Stream: general

Topic: Memory consumption

Yury G. Kudryashov (Jan 30 2020 at 21:41):

Sometimes lean server (started by emacs) starts eating lots of ram (5g and more). Should I do some magic with ulimits, or there is a way to prevent this from inside lean?

Yury G. Kudryashov (Jan 30 2020 at 21:42):

The best way to reproduce the effect is to open a file with many not yet compiled dependencies

Kevin Buzzard (Jan 30 2020 at 21:43):

In VS Code there is an option to give some extra command line inputs, and -M 2000 or something might be what you want

Kevin Buzzard (Jan 30 2020 at 21:44):

$ lean --help
Lean (version 3.4.2, commit cbd2b6686ddb, Release)
  --help -h          display this message
  --version -v       display version number
  --githash          display the git commit hash number used to build this binary
  --run              executes the 'main' definition
  --doc=file -r      generate module documentation based on module doc strings
  --make             create olean files
  --recursive        recursively find *.lean files in directory arguments
  --trust=num -t     trust level (default: max) 0 means do not trust any macro,
                     and type check all imported modules
  --quiet -q         do not print verbose messages
  --memory=num -M    maximum amount of memory that should be used by Lean
                     (in megabytes)

Yury G. Kudryashov (Jan 30 2020 at 21:48):

It runs with -M1024

Kevin Buzzard (Jan 30 2020 at 21:49):

And still eats 5 gigs? :-/

Patrick Massot (Jan 30 2020 at 21:49):

Are you sure you don't have several lean servers started?

Patrick Massot (Jan 30 2020 at 21:50):

Before I upgraded my computer I had this issue when I tried running leanpkg build while VScode was also asking for compilation.

Yury G. Kudryashov (Jan 30 2020 at 21:51):

I'm sure. I run top and see one server process eating all the memory

Yury G. Kudryashov (Jan 30 2020 at 21:51):

I run a locally built 3.5.0

Anne Baanen (Jan 31 2020 at 09:17):

I have this issue with Lean 3.4.2 as well. In addition I've noticed that the Lean server in Emacs doesn't generate olean files making reloading take a lot longer. So usually I run lean --make on the file I want to edit if I changed its dependencies.

Yury G. Kudryashov (Jan 31 2020 at 18:56):

I do the same but sometimes I forget to do this, and lean eats all available ram very quickly.

Last updated: Aug 03 2023 at 10:10 UTC