Parallel proof in ACL2(p)

Here we document support for parallel proof in ACL2(p), an experimental extension of ACL2; also see parallelism, and for parallel programming in particular, see parallel-programming.

- Unsupported-waterfall-parallelism-features
- Proof features not supported with waterfall-parallelism enabled
- Parallel-pushing-of-subgoals-for-induction
- Consequences of how parallelized proofs of subgoals are pushed for induction
- ACL2p-key-checkpoints
- Key checkpoints in ACL2(p)
- Waterfall-parallelism
- For ACL2(p): configuring the parallel execution of the waterfall
- Default-total-parallelism-work-limit
- For ACL2(p): returns the default value for global
total-parallelism-work-limit - Waterfall-printing
- For ACL2(p): configuring the printing within the parallelized waterfall