Out of memory (presumable memory leak) (internal identifier 4)

[icecream17]

Repeating read set.mm and erase results in an Out of memory error:

*** FATAL ERROR:  Out of memory.
Internal identifier (for technical support):  #4 (statement)
To solve this problem, remove some unnecessary statements or file
inclusions to reduce the size of your input source.
Monitor memory periodically with SHOW MEMORY.

This is a sign of a memory leak somewhere. Memory leakage seem to speed up when loading large proofs

input (~test2.txt)

read set.mm
erase
read set.mm
erase
read set.mm
erase
read set.mm
erase
read set.mm
erase
read set.mm
erase
read set.mm
erase
read set.mm
erase
read set.mm
erase
read set.mm
erase
read set.mm
erase
read set.mm
erase
read set.mm
erase
read set.mm
erase
read set.mm
erase
read set.mm
erase
read set.mm
erase
read set.mm
erase
read set.mm
erase
read set.mm
erase
read set.mm
erase

full output

c:\set.mm>metamath
Metamath - Version 0.198 7-Aug-2021           Type HELP for help, EXIT to exit.
MM> sub ~test2.txt
Taking command lines from file "~test2.txt"...
MM> read set.mm
Reading source file "set.mm"... 46059886 bytes
46059886 bytes were read into the source buffer.
The source has 223696 statements; 2846 are $a and 43599 are $p.
No errors were found.  However, proofs were not checked.  Type VERIFY PROOF *
if you want to check them.
MM> erase
Metamath has been reset to the starting state.
MM> read set.mm
Reading source file "set.mm"... 46059886 bytes
46059886 bytes were read into the source buffer.
The source has 223696 statements; 2846 are $a and 43599 are $p.
No errors were found.  However, proofs were not checked.  Type VERIFY PROOF *
if you want to check them.
MM> erase
Metamath has been reset to the starting state.
MM> read set.mm
Reading source file "set.mm"... 46059886 bytes
46059886 bytes were read into the source buffer.
The source has 223696 statements; 2846 are $a and 43599 are $p.
No errors were found.  However, proofs were not checked.  Type VERIFY PROOF *
if you want to check them.
MM> erase
Metamath has been reset to the starting state.
MM> read set.mm
Reading source file "set.mm"... 46059886 bytes
46059886 bytes were read into the source buffer.
The source has 223696 statements; 2846 are $a and 43599 are $p.
No errors were found.  However, proofs were not checked.  Type VERIFY PROOF *
if you want to check them.
MM> erase
Metamath has been reset to the starting state.
MM> read set.mm
Reading source file "set.mm"... 46059886 bytes
46059886 bytes were read into the source buffer.
The source has 223696 statements; 2846 are $a and 43599 are $p.
No errors were found.  However, proofs were not checked.  Type VERIFY PROOF *
if you want to check them.
MM> erase
Metamath has been reset to the starting state.
MM> read set.mm
Reading source file "set.mm"... 46059886 bytes
46059886 bytes were read into the source buffer.
The source has 223696 statements; 2846 are $a and 43599 are $p.
No errors were found.  However, proofs were not checked.  Type VERIFY PROOF *
if you want to check them.
MM> erase
Metamath has been reset to the starting state.
MM> read set.mm
Reading source file "set.mm"... 46059886 bytes
46059886 bytes were read into the source buffer.
The source has 223696 statements; 2846 are $a and 43599 are $p.
No errors were found.  However, proofs were not checked.  Type VERIFY PROOF *
if you want to check them.
MM> erase
Metamath has been reset to the starting state.
MM> read set.mm
Reading source file "set.mm"... 46059886 bytes
46059886 bytes were read into the source buffer.
The source has 223696 statements; 2846 are $a and 43599 are $p.
No errors were found.  However, proofs were not checked.  Type VERIFY PROOF *
if you want to check them.
MM> erase
Metamath has been reset to the starting state.
MM> read set.mm
Reading source file "set.mm"... 46059886 bytes
46059886 bytes were read into the source buffer.
The source has 223696 statements; 2846 are $a and 43599 are $p.
No errors were found.  However, proofs were not checked.  Type VERIFY PROOF *
if you want to check them.
MM> erase
Metamath has been reset to the starting state.
MM> read set.mm
Reading source file "set.mm"... 46059886 bytes
46059886 bytes were read into the source buffer.
The source has 223696 statements; 2846 are $a and 43599 are $p.
No errors were found.  However, proofs were not checked.  Type VERIFY PROOF *
if you want to check them.
MM> erase
Metamath has been reset to the starting state.
MM> read set.mm
Reading source file "set.mm"... 46059886 bytes
46059886 bytes were read into the source buffer.
The source has 223696 statements; 2846 are $a and 43599 are $p.
No errors were found.  However, proofs were not checked.  Type VERIFY PROOF *
if you want to check them.
MM> erase
Metamath has been reset to the starting state.
MM> read set.mm
Reading source file "set.mm"... 46059886 bytes
46059886 bytes were read into the source buffer.
The source has 223696 statements; 2846 are $a and 43599 are $p.
No errors were found.  However, proofs were not checked.  Type VERIFY PROOF *
if you want to check them.
MM> erase
Metamath has been reset to the starting state.
MM> read set.mm
Reading source file "set.mm"... 46059886 bytes
46059886 bytes were read into the source buffer.
The source has 223696 statements; 2846 are $a and 43599 are $p.
No errors were found.  However, proofs were not checked.  Type VERIFY PROOF *
if you want to check them.
MM> erase
Metamath has been reset to the starting state.
MM> read set.mm
Reading source file "set.mm"... 46059886 bytes
46059886 bytes were read into the source buffer.
*** FATAL ERROR:  Out of memory.
Internal identifier (for technical support):  #4 (statement)
To solve this problem, remove some unnecessary statements or file
inclusions to reduce the size of your input source.
Monitor memory periodically with SHOW MEMORY.

Press <return> to exit Metamath.
erase

[twegmann]

Hi @icecream17

Linux Build:
I have checked on WSL with Ubuntu, compiled the latest release and executed more than five of these test2.txt runs.
Using ps -e -opid,vsize,cmd I have monitored the memory consumption of metamath-exe and memory consumption was almost steady (not more than several KB) .

Windows Build:
I could reproduce and debugged with windbg, which was not so successful due to umdh and gflags database issues.
With a new VM running W11 and drmemory I could log all memory allocations but this doesn't really help either, see log.
So a new try would be needed using windbg and proper tracing to (manually) profile the memory de-/allocations.

drmemory_results_dbg_metamath.txt

The issue is likely related to #164

Linux, compiled with gcc

    Metamath - Version 0.199.pre 29-Jan-2022      Type HELP for help, EXIT to exit.
    The program is compiled for a 64-bit CPU.
    sizeof(short)=2, sizeof(int)=4, sizeof(long)=8, sizeof(size_t)=8.

Windows, Metamath exe from website

    Metamath - Version 0.198 7-Aug-2021           Type HELP for help, EXIT to exit.
    The program is compiled for a 32-bit CPU.
    sizeof(short)=2, sizeof(int)=4, sizeof(long)=4, sizeof(size_t)=4.

Windows VM, compiled with lcc

    Metamath - Version 0.199.pre 29-Jan-2022      Type HELP for help, EXIT to exit.
    The program is compiled for a 32-bit CPU.
    sizeof(short)=2, sizeof(int)=4, sizeof(long)=4, sizeof(size_t)=4.

Next steps: Try to Standardize Data Types for Cross-Platform Compatibility:

• Use size_t and ptrdiff_t: Replace instances of long with size_t for sizes and ptrdiff_t for pointer differences (these types accommodate platform-specific pointer sizes, for consistency across 32-bit and 64-bit systems).
• Implement stdint.h Types: Utilize fixed-width integer types from stdint.h (e.g., int32_t, int64_t)