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:

Also available, but optional, are these corresponding extra books, which can be placed in books/ and extracted.

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.