Table of Contents
Thanks to Alex Spiridonov and Jared Davis, a
Windows Installer for ACL2 is available.
The download includes a Unix environment, pre-certified standard and workshop
books, and a copy of Gnu Emacs.
The following times were for the full ACL2 regression suite (distributed
books). Not shown is a successful regression run on Windows using GCL 2.6.7.
In each case below, the first number, User time, is probably the most relevant for
comparisons. The format is essentially:
%Uuser %Ssystem %Eelapsed %PCPU (%Xtext+%Ddata %Mmax)k
%Iinputs+%Ooutputs (%Fmajor+%Rminor)pagefaults %Wswaps
Each of the Linux runs was on the same, almost surely unloaded machine running
Debian GNU/Linux 188.8.131.52.
Note: Noah Friedman has observed that the difference in performance for CLISP
is due to its bytecode-interpreted runtime vs. [for example] GCL's native
object code execution.
- Gnu Common Lisp (GCL), Version 2.6.7:
11728.520u 206.800s 3:24:10.87 97.4% 0+0k 0+0io 0pf+0w
- SBCL 0.98:
19754.766u 486.058s 5:41:29.19 98.7% 0+0k 0+0io 0pf+0w
- Allegro Common Lisp, Version 7.0:
22868.401u 247.715s 6:29:41.28 98.8% 0+0k 0+0io 0pf+0w
- CMUCL 19b:
25064.694u 461.220s 7:10:48.64 98.7% 0+0k 0+0io 4pf+0w
- Lispworks 4.4.6:
33156.124u 251.771s 9:19:58.55 99.4% 0+0k 0+0io 0pf+0w
- CLISP 2.38:
83010.275u 577.688s 23:33:45.72 98.5% 0+0k 0+0io 6pf+0w
Mac OS X times:
Each of the following two Macintosh runs was on the same unloaded Macintosh 2P
G5 running Mac OS 10.4.8.
Each of the following two Macintosh runs was on the same 2 x 3 GHz Dual-Core
Intel Xeon Mac (much faster than the one above), without -j. (Note that the
problem with SBCL seems to persist in SBCL 1.0).
- OpenMCL 1.0 with -j 2:
17540.280u 744.166s 2:41:06.86 189.1% 0+0k 0+6511io 0pf+0w
- SBCL 0.9.12 without -j (apparently cannot run successfully with -j 2):
18362.756u 1516.801s 5:43:16.01 96.5% 0+0k 1+9786io 0pf+0w
Each of the Sun/Solaris runs was on the same Sun4u sparc machine running
- Allegro 6.2:
36753.0u 542.0s 10:29:54 98% 0+0k 0+0io 0pf+0w
- CMUCL 18d:
58865.0u 1597.0s 16:56:57 99% 0+0k 0+0io 0pf+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.
Links to some of J Moore's courses, many of which use ACL2, may be found here.
Here are links to some web pages for a course taught by Rex Page at the
Univ. of Oklahoma.
Eric Smith's web page for a class at Stanford