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

Stream: general

[Scott Morrison]

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]

can you test just one or the other?

[Mario Carneiro]

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

[Scott Morrison]

Will do.

[Mario Carneiro]

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

[Mario Carneiro]

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

[Mario Carneiro]

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]

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]

--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]

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

[Scott Morrison]

So something fishy is going on with --tlean.

[Scott Morrison]

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

[Gabriel Ebner]

https://github.com/leanprover-community/lean/pull/648