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, takes the lesser of that and
physical ram, and runs with that as a heap limit to maximize speed for
the power user. There are several other environment variables which can
tune the gc/allocation algorithms at runtime if you are interested.
Take care,
Adam Borowski writes:
>> > 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 running on the machine. It keeps doing something nasty,
> with garbage collection prominently showing in stack traces.
>
> On a small box, it also hogs most of the memory for itself, being strongly
> anti-social, but finishes successfully.
>
> On a tiny box that's still fine for building any other package, it OOMs.
>
>
> Meow!
--
Camm Maguirec...@maguirefamily.org
==
"The earth is but one country, and mankind its citizens." -- Baha'u'llah
