Zulip Chat Archive

Stream: general

Topic: memory usage with `lean --ast --tlean`

Scott Morrison (Nov 03 2021 at 22:24):

I'm seeing massive memory use while running lean --make --recursive --ast --tlean src on mathlib (exceeding 64gb).

I'm currently trying again with -j4 to see if that helps. In the meantime I'm wondering if there's a memory leak.

  1. @Mario Carneiro, do you have any sense whether this is unlikely/plausible?
  2. I tried running valgrind --undef-value-errors=no --leak-check=yes /Users/scott/.elan/toolchains/lean3-debug/bin/lean --make --recursive --ast --tlean src, but something is wrong with my setup and valgrind isn't actually seeing memory allocations:
==79936== HEAP SUMMARY:
==79936==     in use at exit: 0 bytes in 0 blocks
==79936==   total heap usage: 0 allocs, 0 frees, 0 bytes allocated

Does anyone have experience running valgrind or equivalent on lean, and can point me in the right direction?

Mario Carneiro (Nov 03 2021 at 22:24):

can you test just one or the other?

Mario Carneiro (Nov 03 2021 at 22:24):

i.e. --ast or --tlean, not both

Scott Morrison (Nov 03 2021 at 22:25):

Will do.

Mario Carneiro (Nov 03 2021 at 22:26):

Increased memory usage as a result of --ast is possible, but it's hard to estimate the impact ab initio

Mario Carneiro (Nov 03 2021 at 22:26):

there are a variety of things that can be done to decrease memory usage that were deferred absent evidence of an issue

Mario Carneiro (Nov 03 2021 at 22:28):

If --ast is at fault, it's probably not a memory leak (well I suppose it could be, but it could also just be that we are holding on to a lot of memory)

Scott Morrison (Nov 03 2021 at 23:46):

Okay, it's definitely the --tlean. Compiling with --ast peaks at about 10gb. I've only just started recompiling with --tlean, but it has already blown through 10gb around when it's finished with tactic/.

Mario Carneiro (Nov 04 2021 at 00:47):

--ast already compiles nearly the same information as --tlean, but binport has not yet been adapted to make use of the information. Do you see the same results when compiling with the usual export format?

Scott Morrison (Nov 04 2021 at 01:29):

No, compiling with --export behaves like --ast: looks like it is going to peak around 10gb.

Scott Morrison (Nov 04 2021 at 01:29):

So something fishy is going on with --tlean.

Scott Morrison (Nov 08 2021 at 02:01):

I've noted this as https://github.com/leanprover-community/lean/issues/647

Gabriel Ebner (Nov 08 2021 at 12:37):


Last updated: Aug 03 2023 at 10:10 UTC