Table of Contents
We recommend that you use the latest incremental release, as it contains
The following times were for the full ACL2 regression suite (distributed
books). Not shown is a successful regression run on Windows using GCL.
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 22.214.171.124.
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:
12712.650u 232.366s 3:38:32.41 98.7% 0+0k 0+0io 1pf+0w
- SBCL 0.98:
19496.062u 590.336s 5:37:17.49 99.2% 0+0k 0+0io 0pf+0w
- Allegro Common Lisp, Version 7.0:
20236.888u 187.415s 5:43:06.93 99.2% 0+0k 0+0io 0pf+0w
- CMUCL 19b:
20530.959u 494.658s 5:53:09.77 99.2% 0+0k 0+0io 0pf+0w
28889.313u 243.047s 8:08:04.13 99.4% 0+0k 0+0io 0pf+0w
- CLISP 2.38:
72702.279u 515.380s 20:32:36.02 99.0% 0+0k 0+0io 2pf+0w
Mac OS X times:
Each of the Macintosh runs was on the same unloaded Macintosh 2P G5 running Mac
- OpenMCL 1.0 with -j 2:
23021.449u 879.092s 3:28:30.71 191.0% 0+0k 0+6912io 0pf+0w
- SBCL 0.9.12 without -j (apparently cannot run successfully with -j 2):
23818.622u 2021.217s 7:25:12.69 96.7% 0+0k 0+9797io 0pf+0w
- GCL 2.6.8pre with -j 2:
25229.008u 9517.534s 5:11:23.07 185.9% 0+0k 0+10168io 0pf+0w
Each of the Sun/Solaris runs was on the same reasonably unloaded Sun4u sparc
machine running Solaris 2.9.
- Allegro 6.2:
33600.0u 367.0s 9:56:57 94% 0+0k 0+0io 0pf+0w
- CMUCL 18d:
52551.0u 1579.0s 15:47:15 95% 0+0k 0+0io 0pf+0w
Patch for GCL profiling
We have put up a page providing a fix for a bug
in the procedure for building a profiling ACL2 image on top of GCL. Thanks
to Sol Swords for bringing this bug to our attention.
Contributing Books to ACL2
Please see the email
request for contributing and documenting ACL2 books and the instructions
for contributing books to ACL2.
The POPLmark Challenge
An email has been placed here
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
There is a bug that could affect users of OpenMCL Version 0.14.2 or 0.14.3
under Version 10.4 or 10.4.1 of Mac OS X. You can obtain a fix here, graciously provided by Gary