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), for especially the 64-bit runs, where there may have been other user processes on the machines. Not shown here are a Windows run using GCL 2.6.7. Also, we successfully ran the entire regression suite very shortly before final testing, using safety 3 (CCL).
Statistics shown below for Linux are for running
make
regression on 8-core machines. The -j
8 was used (i.e., up to 8 parallel jobs) for these, so again,
the first number in each case (marked with "u"), User
seconds, is more relevant than the rest. Each Linux 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; others for the
64-bit OS runs. Each Macintosh run used `make/ with
option -j 2, on a 2.4GHz Intel Core 2 Duo with 4 GB of
RAM. NOTE: The 64-bit and Macintosh runs skipped the directory
books/clause-processors/SULFA/, which accounts for about
4 or 5 minutes of User time.
32-bit Linux runs
17938.181u 322.432s 1:01:04.97 498.2% 0+0k 0+0io 132pf+0w
21254.180u 516.276s 1:09:43.23 520.4% 0+0k 0+0io 180pf+0w
15815.248u 654.616s 46:29.32 590.4% 0+0k 0+0io 191pf+0w
19428.502u 660.053s 1:02:40.65 534.1% 0+0k 0+0io 228pf+0w
97118.293u 1012.531s 5:19:13.19 512.3% 0+0k 0+0io 0pf+0w
64-bit Linux runs
17244.829u 416.686s 58:42.27 501.4% 0+0k 0+0io 974pf+0w
17068.386u 1043.093s 53:23.74 565.3% 0+0k 0+0io 1415pf+0w
19829.723u 651.216s 1:04:36.49 528.3% 0+0k 0+0io 1374pf+0w
Macintosh 2.4GHz Intel Core 2 Duo runs
13058.967u 810.848s 2:02:31.65 188.6% 0+0k 0+4632io 1pf+0w
12130.316u 815.137s 1:54:34.20 188.3% 0+0k 0+5227io 2pf+0w
Sun Fire 480R, 1.2GHz, 4 cpus (but using only one cpu), 16G memory
64988.0u 2717.0s 19:02:32 98% 0+0k 0+0io 0pf+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.