ACL2 Version 2.9.2

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.2 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

Finally: Jared Davis has kindly provided a Windows installer for ACL2 Version 2.9.2..

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:
10119.890u 140.310s 2:54:39.16 97.9% 0+0k 0+0io 12231519pf+0w
Allegro Common Lisp, Version 6.2:
14456.560u 172.440s 4:07:50.43 98.3% 0+0k 0+0io 8555056pf+0w
CMUCL 19a:
15172.750u 293.310s 4:23:30.34 97.8% 0+0k 0+0io 9938663pf+0w
CLISP 2.33:
68754.020u 401.530s 19:25:31.69 98.8% 0+0k 0+0io 4019814pf+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.