Major Section: ACL2-BUILT-INS
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 the number of cpu cores if ACL2 can get that information
from the underlying Common Lisp implementation. Otherwise an error occurs,
unless global 'cpu-core-count
is assigned to a positive integer value
(see assign), in which case that value is returned as the core-count
.
Example: (cpu-core-count state) ==> (mv 4 state).