Memory consumption

Stream: general

[Yury G. Kudryashov]

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]

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

[Kevin Buzzard]

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]

$ lean --help
Lean (version 3.4.2, commit cbd2b6686ddb, Release)
Miscellaneous:
  --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]

It runs with -M1024

[Kevin Buzzard]

And still eats 5 gigs? :-/

[Patrick Massot]

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

[Patrick Massot]

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]

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

[Yury G. Kudryashov]

I run a locally built 3.5.0

[Anne Baanen]

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]

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