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. In each case below, the first number, User time in seconds, is probably the best one to use for comparisons (as opposed to System time or Elapsed time), especially for the 64-bit runs, where there were other user processes on the machines. Not shown here are successful runs with CCL 1.2 (1.2-r9226-RC1 DarwinPPC32), SBCL 1.0.2 on a PowerPC Mac; and appropriate Windows runs using GCL 2.6.7 and SBCL 1.0.13 on Windows/MinGW.
All statistics shown below are for running
make
regression on 8-core machines. The -j
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.
32-bit OS runs
18152.178u 309.847s 1:01:17.86 501.9% 0+0k 0+0io 130pf+0w
21718.361u 593.177s 1:10:18.40 528.9% 0+0k 0+0io 177pf+0w
14867.325u 619.074s 45:27.78 567.7% 0+0k 0+0io 193pf+0w
19382.419u 658.269s 1:04:27.71 518.1% 0+0k 0+0io 0pf+0w
97418.104u 989.125s 5:20:03.54 512.4% 0+0k 0+0io 0pf+0w
64-bit OS runs
18057.648u 487.566s 1:05:31.87 471.6% 0+0k 0+0io 951pf+0w
16040.210u 961.560s 57:17.48 494.5% 0+0k 0+0io 1386pf+0w
19620.466u 606.437s 1:09:57.45 481.8% 0+0k 0+0io 1186pf+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.