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. You can place forms to evaluate at start-up into file
init.lsp in the
directory where you are starting ACL2 (GCL), or into file
in your home directory. For example, in order to evaluate both of the lisp
forms mentioned in 2 below, you could put them both into
init.lsp in the
current directory or in
~/acl2-init.lsp (either way, without
(setq si::*optimize-maximum-pages* nil) (si::allocate 'cons 75000 t)
2. 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
3. Windows users have seen this error:
cc1.exe: unrecognized option `-fno-zero-initialized-in-bss'Camm Maguire suggests that a solution may be to evaluate the following in GCL before building ACL2.
(in-package 'compiler) (let* ((x `-fno-zero-initialized-in-bss') (i (search x *cc*))) (setq *cc* (concatenate 'string (subseq *cc* 0 i) (subseq *cc* (+ i (length x))))))
4. It is possible to profile using ACL2 built on GCL. See file
save-gprof.lsp in the ACL2 source directory.