building an ACL2 executable with parallel evaluation enabled
Major Section:  PARALLELISM

See parallel and see parallelism-tutorial for an introduction to parallel evaluation in ACL2 using parallelism primitives pand, por, plet, and pargs.

You can build an experimental version of ACL2 that supports parallel evaluation in the following host Common Lisp implementations:

* CCL (OpenMCL)

* SBCL with threads (feature :sb-thread)

An easy way is to build an executable supporting parallel evaluation is to include the following with a make command:

So for example, to make an executable image and also documentation (which will appear in subdirectories doc/EMACS and doc/HTML):
make large DOC ACL2_PAR=p