For ACL2(p): control the action taken when the thread limit is exceeded
This documentation topic relates to the experimental extension of ACL2 supporting parallel execution and proof; see parallelism.
General Forms: (set-total-parallelism-work-limit-error t) ; cause error (default) (set-total-parallelism-work-limit-error nil) ; disable error and ; continue serially
See parallelism-tutorial, Section ``Another Granularity Issue Related to Thread Limitations'', for an explanation of how the host Lisp can run out of threads. See set-total-parallelism-work-limit for further details, including an explanation of how to manage the limit that triggers this error.
The value of state global
(1) Remove the limit by evaluating the following form.
(2) Disable the error so that execution continues serially once the available thread resources have been exhausted.
(3) Increase the limit on number of threads that ACL2(p) is willing to create, in spite of potential risk (see set-total-parallelism-work-limit). In this case, the following query returns the current limit.
Then to increase that limit, evaluate the following form:
For example, suppose that the value of