INTERNAL PANIC: out of memory

Stream: lean4

[Mac]

I just built Papyrus with the latest nightly (09-12) on Ubuntu WSL, and encountered an INTERNAL PANIC: out of memory error when running one of my tests (i.e., the big script/program.lean test).

Since I just ported Papyrus to the new Lean C API, a bug in the port could be the problem, but the fact the other tests run fine is leading me to suspect that something in Lean changed to case this kind of panic. Also, I am curious what causes this error, because I have never seen it appear before -- even when, for example, encountering stack overflow bugs.

[Leonardo de Moura]

@Mac Lean does generate this error message when it fails to allocate memory.
Did you try to run the program on gdb? You can interrupt the program at lean_internal_panic_out_of_memory, and traverse the stack trace.

[Mac]

Ah, thanks for the advice, will do!

[Mac]

As it turns out, it was a bug on my end. :upside_down: I am still a little surprised I had never encountered an INTERNAL PANIC before with similar bugs. However, fixing that has lead to different error -- this time with the mpz code.

@Leonardo de Moura, shouldn't the mpz_t of lean_extract_mpz_value be a pointer (or, on the C++, side a reference) like it is for the other mpz_t methods? I think that may explain the segfault I'm getting (which I have verified is coming from the use of lean_extract_mpz_value).

[Leonardo de Moura]

@Mac I didn't want to give the pointer to the mpz_t for two reasons. First, the user would be able to modify the value that is stored in the Lean object. Second, if one day we use a different library to implement big nums, we would break the API: we would have to allocate an mpz_t and add function for deleting it. The style I used is the one used by GMP. https://gmplib.org/manual/Assigning-Integers
Note that you have to initialize mpz_t values using void mpz_init (mpz_t x) before invoking lean_extract_mpz_value.

[Mac]

@Leonardo de Moura You beat me to the punch! Here was the response I was drafting (which you essentially already answered):

Oops, scratch that, found the bug. It appears that mpz_set (which lean_extract_mpz_value) uses internally requires that the mpz object be initialized first (e.g., with mpz_init). :upside_down:

However, part of the reason this is necessary is that it appears that mpz_set is performing a deep copy. wo copies in a row on the same data (one to get the mpz data from Lean, one to copy it into a LLVM APInt) seems kind of wasteful. Would it be possible for the API to perform a shallow copy (by assigning the numeric's mpz_t to a pointer argument via =). Or, alternatively, just to return the numeric's pointer directly?

[Mac]

Leonardo de Moura said:

Second, if one day we use a different library to implement big nums, we would break the API: we would have to allocate an mpz_t and add function for deleting it.

Oh well, I guess that makes sense. I am just happy that it works now! :wink: However, you may want to add a note to the lean_extract_mpz_value comment that mentions the mpz_t needs to already be initialized (as the only way an end-user would discover that currently is by inspecting the implementation).

[Mac]

(though I guess the fact it uses mpz_set may be implied by the particular word choice of 'set' in the comment.)

[Kitty Gorey]

Not sure if this is the right place to ask this but how much memory does Lean need? I followed the instructions on https://leanprover-community.github.io/install/project.html and VSCode slowly use more and more of my (laughable) ~4GB of usable RAM. Once VSCode has around 2048MB of memory used up my computer just starts acting like it's on its deathbed. Is this normal?

[Kevin Buzzard]

This isn't a question about lean 4 so doesn't go here (please send any further responses to the #new membersstream so as not to derail this thread any further), but the short answer is that if you want to use lean 3's maths library mathlib then right now you will struggle in practice with anything less than 16 gigs of ram, although some people do get by with 8.