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
#+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