ACL2 Version 2.9.4

Incremental release 2.9.4 of ACL2 is available, as described in an announcement already sent to the acl2 mailing list by email.

We have put on the web the Version 2.9.4 home page, documentation, and release notes.

Downloads:

acl2.tar.gz: ACL2 2.9.4 gzipped tarball
acl2-tar-gz-md5sum: corresponding md5sum file
patches/: optional patch files

Also available, but optional, are these corresponding extra books, which can be placed in books/ and extracted. You will not be able to use previous versions of these books with a new incremental release, so if you want to use these books, be sure to fetch the tarballs!

workshops.tar.gz: Workshops tarball
workshops-tar-gz-md5sum: corresponding md5sum file
nonstd.tar.gz: ACL2(r) books tarball
nonstd-tar-gz-md5sum: corresponding md5sum file

Performance Comparisons

The following times are for certifying the full ACL2 regression suite (distributed and workshop books). The comparisons give an idea of relative performance of ACL2 built on these lisps, but are not necessarily representative of their general performance for other than ACL2. For example, ACL2 handles multiple values in at least 3 different ways depending on the underlying lisp, and it proclaims functions in some lisps but not others.

The first set of numbers, immediately below, are from a 1-processor 2.60 GHz Pentium 4 with a 512 KB cache, running Linux (Ubuntu 5.10). 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

Gnu Common Lisp (GCL), Version 2.6.6:
11791.744u 201.456s 3:22:34.21 98.6% 0+0k 0+0io 0pf+0w
SBCL 0.9.5:
18496.823u 1054.073s 5:27:45.79 99.4% 0+0k 0+0io 0pf+0w
Allegro Common Lisp, Version 7.0:
18808.655u 190.663s 5:19:18.79 99.1% 0+0k 0+0io 0pf+0w
CMUCL 19b:
19127.743u 484.590s 5:29:13.82 99.2% 0+0k 0+0io 0pf+0w
LispWorks 4.4.5:
26807.411u 223.009s 7:34:21.79 99.1% 0+0k 0+0io 0pf+0w
CLISP 2.34:
69597.653u 495.854s 19:55:10.62 97.7% 0+0k 0+0io 0pf+0w

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.

The second set of numbers is for runs on a 2-processor 2.7 GHz Macintosh PowerPC G5 with 512K cache per processor and 8GB of RAM, where the runs took advantage of both processors by invoking "make -j 3".


OpenMCL 1.0:

real	153m59.139s
user	276m30.983s
sys	11m19.956s

GCL 2.6.8 preliminary version:

real	277m31.000s
user	362m15.690s
sys	143m44.793s

Pete Manolios reported the following times for the distributed books on a Mac OS X system with a dual 2.7 GhZ PowerPC G% and 6.5GB DDR SDRAM.

openmcl: 126m5.739s 
sbcl:    135m47.669s