ACL2 Version 3.1 News

Table of Contents

Windows Installer

Thanks to Alex Spiridonov and Jared Davis, a Windows Installer for ACL2 is available. The download includes a Unix environment, pre-certified standard and workshop books, and a copy of Gnu Emacs.

Performance Comparisons

The following times were for the full ACL2 regression suite (distributed and workshop books). Not shown is a successful regression run on Windows using GCL 2.6.7.

In each case 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

Linux times:

Each of the Linux runs was on the same, almost surely unloaded machine running Debian GNU/Linux 2.6.17.4. 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.

Mac OS X times:

Each of the following two Macintosh runs was on the same unloaded Macintosh 2P G5 running Mac OS 10.4.8. Each of the following two Macintosh runs was on the same 2 x 3 GHz Dual-Core Intel Xeon Mac (much faster than the one above), without -j. (Note that the problem with SBCL seems to persist in SBCL 1.0).

Sun/Solaris times:

Each of the Sun/Solaris runs was on the same Sun4u sparc machine running Solaris 2.9.

ACL2 Course Materials

At some point, perhaps "ACL2 Course Materials" will be a top-level link on the ACL2 home page. For now, we provide some links.