ACL2 Version 2.9.1

The first 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.1 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.

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.5:
9762.890u 145.470s 2:50:18.21 96.9% 0+0k 0+0io 12521954pf+0w
Allegro Common Lisp, Version 6.2:
13997.980u 172.160s 4:03:13.73 97.0% 0+0k 0+0io 9075727pf+0w
CMUCL 19a:
14896.620u 296.230s 4:29:07.95 94.0% 0+0k 0+0io 10445178pf+0w
CLISP 2.33:
66727.350u 405.390s 19:00:17.83 98.1% 0+0k 0+0io 4620602pf+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.