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.
We have fixed bugs in the handling of
expressions, one of which had the capability of rendering ACL2
unsound. Thanks to Sol Swords for his help in identifying these
problems. To read more and download the patch file, which includes
installation instructions, visit:
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. In each case below, the first number, User time in seconds, is by far the best one to use for comparisons (as opposed to System time or Elapsed time). Not shown here are successful runs on several other platforms: Lispworks 4.4.6 on 32-bit Ubuntu Linux; CMU Common Lisp 18d on Sun/Solaris (SunOS 5.9); CCL 1.2 (1.2-r9918M-trunk DarwinPPC32) and SBCL 1.0.2 on a PowerPC Mac; and GCL 2.6.7 and SBCL 1.0.13 on Windows/MinGW.
All statistics shown below are for running
regression on 8-core machines. The
8 was used (i.e., up to 8 parallel jobs), so again, the first
number in each case (marked with "
u"), User seconds, is
more relevant than the rest. Each regression run was on a 2.2 GHz AMD
Opteron (tm) Processor 850 running Ubuntu Linux. One such machine was
used for the 32-bit OS runs; another for 64-bit OS runs. NOTE: The
64-bit runs skipped the directory
books/clause-processors/SULFA/, which accounts for about
4 or 5 minutes of User time; so the GCL penalty for 64-bit linux may
be greater than appears below.
32-bit OS runs
10775.357u 538.793s 34:29.15 546.8% 0+0k 0+0io 868pf+0w
11820.018u 258.680s 38:01.23 529.4% 0+0k 0+0io 671pf+0w
15751.688u 495.538s 50:45.49 533.4% 0+0k 0+0io 1723pf+0w
67041.405u 776.160s 3:48:57.35 493.6% 0+0k 0+0io 0pf+0w
64-bit OS runs
11314.551u 716.868s 34:58.16 573.4% 0+0k 0+0io 1795pf+0w
12628.561u 175.486s 41:02.47 519.9% 0+0k 0+0io 1158pf+0w
14076.155u 408.825s 45:15.77 533.3% 0+0k 0+0io 2597pf+0w
ACL2 Course Materials
At some point, perhaps "ACL2 Course Materials" will be a top-level link on the
ACL2 home page. For now, we provide some links.