This site is for community-driven development for the basic ACL2 libraries, which deal with topics like arithmetic, data structures, and hardware modelling. We're working with the authors of ACL2 and our changes are eventually incorporated into official ACL2 releases.
The various cases below correspond to runs of the ACL2 regression suite (distributed and workshop books) for ACL2 executables built on different platforms, as indicated. Not shown are results of testing on Windows and Mac OS X or of running with safety 3 using CCL.
Statistics shown below are for running
Each 32-bit Linux regression reported below was run with
-j 8 on an 8-core 2.2 GHz AMD
Opteron (tm) Processor 850 running Ubuntu Linux. Each 64-bit Linux
regression reported below was run with
-j 24 on a 2.6GHz machine with four processors, each a
Six-Core AMD Opteron(tm) Processor 8435. Also, the 64-bit runs
skipped directory books/clause-processors/SULFA/. So comparisons
between a 32-bit run and 64-bit run are ill-advised.
21507.912u 391.984s 1:18:32.06 464.7% 0+0k 0+968536io 0pf+0w
26377.076u 409.081s 1:39:44.37 447.6% 0+0k 169240+915072io 216pf+0w
22751.109u 1088.488s 1:12:12.10 550.3% 0+0k 114952+2174256io 0pf+0w
25421.292u 1571.322s 1:36:34.76 465.8% 0+0k 182680+1074336io 243pf+0w
workshops/books. The user time alone was 66869.515u.
17874.477u 310.343s 1:08:15.93 443.9% 0+0k 253168+656968io 1197pf+0w
45138.004u 2625.456s 1:20:57.38 983.3% 0+0k 335608+1997728io 0pf+0w
22349.060u 1172.229s 1:01:30.15 637.4% 0+0k 56936+837904io 0pf+0w
ACL2 Course Materials
At some point, perhaps "ACL2 Course Materials" may be a top-level link on the
ACL2 home page. For now, we provide some links.