Major Section: PARALLELISM
This documentation topic relates to the experimental extension of ACL2 supporting parallel execution and proof; see parallelism. See parallelism-tutorial for an introduction to parallel programming in ACL2.
You can build an experimental version of ACL2 that supports parallel execution in the following host Common Lisp implementations:
* CCL (OpenMCL)
* Lispworks 6.0
* SBCL with threads (feature
:sb-thread)
The command below will compile ACL2 to support parallel execution, including
parallel execution during proofs. Any non-empty string may be used in place
of t, and the value of LISP (shown here as ccl) is any Lisp
executable on which one can build ACL2(p) (see parallelism).
make ACL2_PAR=t LISP=ccl
So for example, to make an executable image and also documentation (which
will appear in subdirectories doc/EMACS and doc/HTML), using the Lisp
executable ccl:
make large DOC ACL2_PAR=t LISP=ccl
