For ACL2(p): using waterfall parallelism during book certification
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.
(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