ACL2 Version 3.0 News

Table of Contents

Incremental Releases

We recommend that you use the latest incremental release, as it contains significant improvements.

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.

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.13.2. 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 Macintosh runs was on the same unloaded Macintosh 2P G5 running Mac OS 10.4.5.

Sun/Solaris times:

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

Patch for GCL profiling

We have put up a page providing a fix for a bug in the procedure for building a profiling ACL2 image on top of GCL. Thanks to Sol Swords for bringing this bug to our attention.

Contributing Books to ACL2

Please see the email request for contributing and documenting ACL2 books and the instructions for contributing books to ACL2.

The POPLmark Challenge

An email has been placed here

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.

OpenMCL patch

There is a bug that could affect users of OpenMCL Version 0.14.2 or 0.14.3 under Version 10.4 or 10.4.1 of Mac OS X. You can obtain a fix here, graciously provided by Gary Byers.

GCL Tips