Major Section: PARALLELISM
This documentation topic relates to the experimental extension of ACL2 supporting parallel execution and proof; see parallelism.
There are books whose certification can be sped up significantly by using
waterfall parallelism. (See parallelism, including the caveat in its
"IMPORTANT NOTE".) One such example in the ACL2 community books is
models/jvm/m5/apprentice.lisp, which is typically excluded from
regressions because of how long it takes to certify. In order to use
waterfall parallelism during certification of a book <book-name>.lisp
using `make' (see books-certification and see books-certification-classic),
we recommend creating a file <book-name>.acl2 that includes the following
forms.
#+acl2-par (set-waterfall-parallelism t) (certify-book <book-name> ? t) ; other arguments may be preferable
Note that there are books that will not certify when waterfall-parallelism is
enabled. See file acl2-customization-files/README for more information,
including how to certify essentially all books using waterfall
parallelism.
