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,
'cpu-core-count is assigned to a positive integer value
(see assign), in which case that value is returned as the
Example: (cpu-core-count state) ==> (mv 4 state).