non-parallel-book

(in-package "ACL2")

(defsection non-parallel-book
  :parents (parallelism)
  :short "Mark a book as incompatible with ACL2(p) waterfall parallelism."
  :long "<p>Some features of ACL2 are incompatible with ACL2(p); see @(see
 unsupported-waterfall-parallelism-features).  For example, ACL2(p) does not
 support @(see clause-processor)s that modify the ACL2 @(see state).</p>

 <p>The form @('(non-parallel-book)') instructs ACL2 to ensure that @(see
 waterfall-parallelism) is turned off.  When you put that form into a book, it
 will be ignored when including the book unless keyword @(':check-expansion')
 is true.  (Suggestion: avoid that keyword unless you are sure you know what
 you are doing!)</p>"
  (defmacro non-parallel-book
    (&key check-expansion)
    `(make-event (if (f-get-global 'parallel-execution-enabled state)
        (er-progn (set-waterfall-parallelism nil)
          (value '(value-triple nil)))
        (value '(value-triple nil)))
      ,@(AND CHECK-EXPANSION '(:CHECK-EXPANSION T)))))