ACL2 Version 2.9.3

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

Click here for a text-only copy of the release notes. For the full updated documentation, download the release:

acl2.tar.gz: ACL2 2.9.3 gzipped tarball
acl2-tar-gz-md5sum: corresponding md5sum file

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 were for the full ACL2 regression suite (distributed and workshop books), on the same, almost surely unloaded, x86 machine running Debian GNU/Linux.

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

Gnu Common Lisp (GCL), Version 2.6.6:
10104.050u 141.970s 2:54:21.31 97.9% 0+0k 0+0io 12346498pf+0w
Allegro Common Lisp, Version 7.0:
16404.010u 218.520s 4:41:19.96 98.4% 0+0k 0+0io 15676143pf+0w
CMUCL 19b:
16168.410u 318.290s 4:40:56.51 97.8% 0+0k 0+0io 10100310pf+0w
CLISP 2.33:
67807.360u 406.300s 19:06:00.41 99.2% 0+0k 0+0io 4034939pf+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.