COMPILING-ACL2P

compiling ACL2(p)
Major Section:  PARALLELISM

This documentation topic relates to the experimental extension of ACL2 supporting parallel evaluation and proof; see parallelism. See parallel and see parallelism-tutorial for an introduction to parallel programming in ACL2 using primitives plet, pargs, pand, por, and spec-mv-let.

You can build an experimental version of ACL2 that supports parallel evaluation 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