GCL

tips on building and using ACL2 based on Gnu Common Lisp 
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 acl2-init.lsp 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 (lp) or :q): 

(setq si::*optimize-maximum-pages* nil)
(si::allocate 'cons 75000 t)
Note that if you want to put ACL2 patches in this file, you should precede them with (in-package "ACL2").

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 loop
A 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
Also see reset-kill-ring for a suggestion on how to free up space.

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.

5. Some versions of GCL may have garbage-collector bugs that, on rare occasions, cause ACL2 (when built on GCL) to break. If you run into this, a solution may be to execute the following: 

:q
(si::sgc-on nil)
(lp)
Alternatively, put (si::sgc-on nil) in your ~/acl2-init.lsp file.

A full regression test and found that this decreased performance by about 10%. But even with that, GCL is probably one of the faster Common Lisp implementations for ACL2 on Linux. Performance figures may often be found by following the ``Recent changes'' link on the ACL2 home page.

6. GCL operations on numbers can sometimes be sped up, perhaps by up to two orders of magnitude, by suitable declare forms (also see type-spec). The following example, developed with Warren Hunt and Serita Nelesen, illustrates the use of such declarations.

; File iplus.lisp:
; Operations on naturals together with positive infinity (represented as -1).

; After (ld "iplus.lisp"), escape to raw Lisp with :q and then eavluate
; (disassemble 'big-test).  You should see lots of arithmetic operations
; in C code, but no calls of C functions CMPmake_fixnum or number_plus.

(in-package "ACL2")

(defmacro i-max ()
  (expt 2 (1- 28)))

(defmacro i+ (x y)
  `(the (signed-byte 28)
        (let ((x ,x)
              (y ,y))
          (declare (type (signed-byte 28) x y))
          (cond ((or (< x 0)
                     (< y 0))
                 -1)
                (t (let ((result
                          (the (signed-byte 29) (+ x y))))
                     (declare (type (signed-byte 29) result))
                     (cond ((>= result (i-max)) -1)
                           (t (the (signed-byte 28) result)))))))))

(defmacro imin (x y)
  `(the (signed-byte 28)
        (let ((x ,x)
              (y ,y))
          (declare (type (signed-byte 28) x y))
          (cond ((< x 0)
                 (cond ((< y 0) -1)
                       (t y)))
                ((< y 0)
                 x)
                (t
                 (the (signed-byte 28) (min x y)))))))

(defun big-test (x y z)
  (declare (type (signed-byte 28) x y z))
  (imin (i+ x y)
        (i+ y (imin x z))))