		Search-engine friendly clone of the ACL2 documentation.

Ccl-installation

Ccl-installation-extra

Clozure Common Lisp (CCL) installation and implementation details

NOTE: See the Clozure CL releases page for the latest information, which may supersede some of what is included below.

This topic, contributed by Warren A. Hunt, Jr., extends the basic information given in ccl-installation. It may be useful to some, especially those who use ACL2 in ways that particularly stress memory. Another resource may be found on this page.

Below we provide instructions to build CCL on FreeBSD and MacOS; building on Linux will be similar. Before providing the build instructions, we mention a few facts about CCL's implementation.

CCL's implementation can't expand stack space automatically. The sizes of various stacks are set at thread creation time. Most programs don't need very big stacks. The CCL default value and temp stack sizes may be too small for compute-intensive applications.

The various stack sizes are set when creating a thread with code in CCL::MAKE-PROCESS and CCL::PROCESS-RUN-FUNCTION, and they set the three stack sizes of the initial listener thread that is created when CCL starts.

The value stack is used for data in deeply-nested lisp recursion. ACL2 can benefit from an increase in the size of the value stack.

The temp stack is used for dynamic-extent objects. This might need need to be larger than the default.

The control stack is used to run C and binary code; it would be surprising to need to increase its size.

If only one or two threads are needed, giant (e.g., 4 GB) stacks can be OK, but with many threads large stacks use lots of memory. Below are the stacks along with their current (April, 2020) default sizes.

ccl::*default-control-stack-size*                    ;; default 2^21
ccl::*initial-listener-default-control-stack-size*   ;; default 2^21

ccl::*default-value-stack-size*                      ;; default 2^21
ccl::*initial-listener-default-value-stack-size*     ;; default 2^21

ccl::*initial-listener-default-temp-stack-size*      ;; default 2^20
ccl::*default-temp-stack-size*                       ;; default 2^20

If we are running on a 32-bit platform, we set the stack sizes modestly. If we are on a 64-bit platform, we set the stack sizes to much larger values. See the later discussion about ``configure-ccl.lisp'' below to see how to alter (increase) stack sizes.

MacOS Build Instructions:

git clone https://github.com/Clozure/ccl.git ccl-dev
curl -L -O https://github.com/Clozure/ccl/releases/download/v1.12-dev.5/darwinx86.tar.gz
cd ccl-dev ; tar xf ../darwinx86.tar.gz

Rebuild C-based, Lisp kernel

To rebuild the Lisp-code part of the kernel, do...

cd lisp-kernel/darwinx8664 ; make ; cd ../..

Unlike for FreeBSD and Linux, we exclude ``:full t'' from the ``rebuild-ccl'' command just below Matt Emerson (a CCL expert) writes:

After looking at your log, I was able to duplicate the problem myself. For some reason I do not understand, it appears that on Catalina, removing the running lisp kernel binary causes run-program to break (trying to run external programs gets signal 9). This surprises me very much.

One of the effects of running (rebuild-ccl :full t), is that it first does a "make clean" in the lisp kernel directory, and then does a regular make. This has worked for years, and I do not know why it has stopped working.

To avoid this, rebuild the lisp with (rebuild-ccl :clean t) instead. Do not specify ``:full t''. Since you have already built the lisp kernel, you gain nothing from ``:full t'' doing it again. So, once the C-based, Lisp kernel is built, then do:

echo "(in-package :ccl) (rebuild-ccl :verbose t :clean t)" | \
      ./dx86cl64 -n |& tee ./ccl-build-compile.log

Matt Emerson suggests that one re-build again. We asked Matt a long-simmering question: we have been told that it is a good idea to compile CCL twice. Is that so that the CCL compiler produced by pass one on the target system is used to compile the CCL system that will be used (on the target system)? Or, is compiling twice some silly myth? Matt Emerson responded:

It's not entirely mythic. Some rare changes do need the lisp to be rebuilt twice for bootstrapping purposes, but usually it isn't required.

Thus, we recommend you re-build (compile) the Lisp code again.

echo "(in-package :ccl) (rebuild-ccl :verbose t :clean t)" | \
      ./dx86cl64 -n |& tee ./ccl-build-compile-2.log

Finally, one may specialize the final image by:

cat configure-ccl.lisp | ./dx86cl64 -n |& tee ~/ccl-build-specialize.log

where ``configure-ccl.lisp'' (not supplied) contains whatever CCL specialization commands you wish to have in the version of CCL you use for ACL2 or other work. See the end of this note for an example of ``configure-ccl.lisp''.

FreeBSD Build Instructions:

The FreeBSD build instructions are similar to the MacOS build instruction, but the names are changed appropriately.

git clone https://github.com/Clozure/ccl.git ccl-dev
curl -L -O https://github.com/Clozure/ccl/releases/download/v1.12-dev.5/freebsd12-x8664.tar.gz
cd ccl-dev
tar xf ../freebsd12-x8664.tar.gz

Rebuild C-based Lisp kernel

cd lisp-kernel/freebsdx8664 ; make ; cd ../..

To rebuild the Lisp-code part of the kernel, do...

echo "(in-package :ccl) (rebuild-ccl :full t :verbose t :clean t)" | \
      ./fx86cl64 -n |& tee ./ccl-build-compile.log

FreeBSD is OK with the ``:full t'' flag, which as of MacOS 10.15 breaks (but used to work on earlier versions of MacOS). So, this option persists on the FreeBSD build.

Matt Emerson recommends building the Lisp code a second time; see the ``MacOS Build Instructions'' above for his rationale.

echo "(in-package :ccl) (rebuild-ccl :full t :verbose t :clean t)" | \
      ./fx86cl64 -n |& tee ./ccl-build-compile-2.log

Finally, one may specialize the final image by:

cat ~/a/scripts/configure-ccl.lisp | ./fx86cl64 -n |& tee ~/ccl-build-specialize.log

where ``configure-ccl.lisp'' (not supplied) contains whatever CCL specialization commands you wish to have in the version of CCL you use for ACL2 or other work.

configure-ccl.lisp

Sample ``configure-ccl.lisp'' file for 64-bit implementation:

(progn
  ;; Parameters to configure CCL for use on FreeBSD and MacOS

  (in-package :ccl)

  ;; Enlarge stack sizes
  (setq *default-value-stack-size*                    (expt 2 28))
  (setq *initial-listener-value-stack-size*           (expt 2 28))

  (setq *default-temp-stack-size*                     (expt 2 24))
  (setq *initial-listener-temp-stack-size*            (expt 2 24))

  (setq *default-control-stack-size*                  (expt 2 24))
  (setq *initial-listener-default-control-stack-size* (expt 2 24))

  ;; For CCL double precision
  (setf *read-default-float-format* 'double-float)

  ;; Make DEFUN save the source code for later recovery via
  ;; FUNCTION-LAMBDA-EXPRESSION.
  (setq *save-definitions* t)
  (setq *fasl-save-definitions* t)

  ;; Make GC verbose; see ACL2 documentation topic GC-VERBOSE.
  (gc-verbose t t)

  ;; Dump executable heap image; see ACL2 documentation topic SAVE-EXEC.
  (save-exec *heap-image-name* "Modification string to print at startup")
  )