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:

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!

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