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
regression using community books
the acl2-books project
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 Ubuntu Linux.
workshops/books. The wall clock time for CLISP was about 3 hours, which far exceeded each time just below, even though those below include certification of the
21441.020u 673.790s 1:04:39.14 570.0% 0+0k 234608+1315736io 768pf+0w
23007.590u 447.510s 1:08:33.47 570.2% 0+0k 0+1382848io 0pf+0w
24748.380u 794.960s 1:11:16.18 597.3% 0+0k 111144+3359312io 0pf+0w
26047.770u 539.310s 1:19:39.55 556.2% 0+0k 440864+1647352io 1385pf+0w
27708.360u 490.800s 1:27:20.94 538.0% 0+0k 0+1483824io 0pf+0w
23729.300u 1261.790s 1:19:04.96 526.6% 0+0k 168+1550192io 0pf+0w
25299.000u 507.560s 1:21:53.34 525.2% 0+0k 0+1533992io 0pf+0w
29354.590u 817.940s 1:34:42.05 531.0% 0+0k 499552+1834872io 1447pf+0w
34136.440u 565.450s 2:07:49.23 452.4% 0+0k 199352+1645720io 674pf+0w
29908.985u 710.528s 1:33:28.86 545.9% 0+0k 69800+3164088io 0pf+0w
34357.779u 509.415s 1:44:45.70 554.7% 0+0k 10064+1310624io 1pf+0w
79225.199u 1170.889s 4:02:15.93 553.0% 0+0k 179648+1601920io 507pf+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.