Greetings! You can limit the memory accessible to any GCL based process
by a factor of 0.5 via
export GCL_MEM_MULTIPLE=0.5
The algorithm *is* supposed to avoid OOM, however, so if there are
reproducible details on that I could try to look into it.
GCL probes the brk'able memory at startup,
> > VM with 64 cores
> Neither ACL2 nor underlying gcl makes any use of threads or locks
I assume the 64-core box has adequate memory as well.
For me, also on a 64-core box with "only" 128GB RAM, acl2 takes a
three-digit number of gigs for itself, ignoring any other processes
that are also
2 matches
Mail list logo
