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 by far the best one to use for comparisons (as opposed to System time or Elapsed time). Not shown here are tests of the ACL2 regression suite, all successful, on several other platforms: Lispworks 4.4.6 on 32-bit Ubuntu Linux, Allegro CL 6.2 and CMU Common Lisp 18d on Sun/Solaris (SunOS 5.9), and OpenMCL 1.1 snapshot r7591 on Darwin for Intel-based Mac.
All statistics shown below are for running
make regression. The
-j 6 was used (i.e., up to 6 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 2GHz 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 penalty for 64 bits may be even
greater than appears below.
32-bit OS runs
8955.947u 467.549s 33:59.51 462.0% 0+0k 0+0io 0pf+0w
11000.399u 261.616s 42:36.91 440.4% 0+0k 0+0io 0pf+0w
14785.108u 497.315s 59:28.01 428.3% 0+0k 0+0io 1564pf+0w
62788.912u 739.046s 3:55:09.85 450.2% 0+0k 0+0io 0pf+0w64-bit OS runs
9839.250u 592.925s 35:30.12 489.7% 0+0k 0+0io 1535pf+0w
11548.757u 162.098s 41:59.53 464.8% 0+0k 0+0io 1218pf+0w
13483.606u 371.179s 49:57.39 462.2% 0+0k 0+0io 1359pf+0wACL2 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.