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 statistics below correspond to runs of make -j 8
regression using both distributed and workshop books,
skipping directory books/clause-processors/SULFA/, for
ACL2 executables built on Linux platforms as indicated. Not shown are
results of testing on Windows and Mac OS X or of running a near-final
version with safety 3 using CCL. Each regression was run on an 8-core
2.2 GHz AMD Opteron (tm) Processor 850 running Ubuntu Linux.
19521.139u 397.564s 1:11:05.35 466.9% 0+0k 0+718296io 0pf+0w
25446.370u 432.955s 1:31:57.50 469.0% 0+0k 141032+665344io 220pf+0w
19144.804u 879.342s 1:03:22.29 526.6% 0+0k 171936+1936320io 221pf+0w
25536.751u 1562.801s 1:36:52.92 466.1% 0+0k 182368+821480io 253pf+0w
workshops/ books. The user time alone was 81,538
seconds, far exceeding each of the three user times below even though
those include certification of the workshops/ books.
22844.615u 473.973s 1:22:37.07 470.4% 0+0k 221896+667288io 1219pf+0w
23750.628u 1208.235s 1:19:17.32 524.6% 0+0k 453696+2044464io 1491pf+0w
22808.873u 753.435s 1:24:06.27 466.9% 0+0k 353168+849464io 1754pf+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.