Cpu-core-count
The number of cpu cores
This documentation topic relates to the experimental
extension of ACL2 supporting parallel execution and proof; see parallelism.
Unless the ACL2 executable supports parallel execution (see parallelism), this function returns (mv 1 state). Otherwise:
(Cpu-core-count state) returns (mv core-count state), where
core-count is determined as follows. If environment variable
ACL2_CORE_COUNT has a non-empty value, then that value should represent a
positive integer (else an error occurs), which is the returned
core-count. Otherwise, the returned core-count may be obtained from
the underlying Common Lisp implementation, else as a positive integer value
from state global variable 'cpu-core-count (see assign).
Otherwise an error occurs.
Example:
(cpu-core-count state) ==> (mv 4 state)
Cpu-core-count has the following logical definition.
Function: cpu-core-count
(defun cpu-core-count (state)
(declare (xargs :stobjs state :guard t))
(mv-let (nullp val state)
(read-acl2-oracle state)
(declare (ignore nullp))
(mv val state)))
