• Top
  • Documentation
  • Books
  • Boolean-reasoning
  • Projects
  • Debugging
  • Std
  • Proof-automation
  • Macro-libraries
  • ACL2
    • Theories
    • Rule-classes
    • Proof-builder
    • Recursion-and-induction
    • Hons-and-memoization
    • Events
    • Parallelism
      • Set-waterfall-parallelism
      • Parallel-programming
      • Set-waterfall-printing
      • Unsupported-parallelism-features
      • Set-total-parallelism-work-limit
      • Set-parallel-execution
      • Set-total-parallelism-work-limit-error
      • Compiling-ACL2p
      • Waterfall-parallelism-for-book-certification
      • Cpu-core-count
      • Set-waterfall-parallelism-hacks-enabled
      • Parallel-proof
      • Non-parallel-book
      • Parallel
      • Without-waterfall-parallelism
      • Set-waterfall-parallelism-hacks-enabled!
      • With-waterfall-parallelism
      • Parallelism-build
    • History
    • Programming
    • Operational-semantics
    • Real
    • Start-here
    • Debugging
    • Miscellaneous
    • Output-controls
    • Macros
    • Interfacing-tools
  • Interfacing-tools
  • Hardware-verification
  • Software-verification
  • Math
  • Testing-utilities

• Parallelism

Compiling-ACL2p

Compiling ACL2(p)

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