Major Section: MISCELLANEOUS
See the installation instructions for basic information about building ACL2 on top of GCL, including information about where to fetch GCL. Here, we provide some tips that may be useful.
1. Suppose you run out of space, for example with an error like this:
Error: The storage for CONS is exhausted. Currently, 59470 pages are allocated. Use ALLOCATE to expand the space.The following suggestion from Camm Maguire will minimize the heap size, at the cost of more garbage collection time.
:q ; exit the ACL2 loop (setq si::*optimize-maximum-pages* nil) (lp) ; re-enter the ACL2 loopA second thing to try, suggested by several people, is to preallocate more pages before the run, e.g.:
:q ; exit the ACL2 loop (si::allocate 'cons 75000 t) (lp) ; re-enter the ACL2 loop