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. Each regression was
run on an 8-core Intel Xeon running Ubuntu Linux, with a slightly
faster processor speed on the 32-bit machine (see below).
15944.300u 228.110s 48:14.61 558.7% 0+0k 94576+793080io 150pf+0w
18283.566u 258.204s 55:02.13 561.5% 0+0k 480+756320io 1pf+0w
14454.323u 458.472s 48:51.07 508.7% 0+0k 208416+2054888io 222pf+0w
36019.951u 732.773s 1:49:16.34 560.5% 0+0k 194984+917408io 234pf+0w
workshops/ books. The user time alone was 33,335.040
seconds, exceeding all the user times below even though those below
include certification of the workshops/ books.
13278.780u 341.670s 41:56.86 541.1% 0+0k 312+759200io 0pf+0w
24095.970u 1225.010s 1:41:43.22 414.8% 0+0k 311456+2176112io 393pf+0w
11115.260u 301.640s 34:57.34 544.3% 0+0k 190712+811448io 306pf+0w
15879.580u 579.900s 51:55.10 528.3% 0+0k 395584+974688io 587pf+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.