ACL2 Version 3.4 News

Table of Contents

ACL2 Books Repository

The acl2-books Google group allows you to contribute ACL2 books (input files), and also to update to the latest version if you don't want to wait for the next ACL2 release. Quoting from that web site:
This site is for community-driven development for the basic ACL2 libraries, which deal with topics like arithmetic, data structures, and hardware modelling. We're working with the authors of ACL2 and our changes are eventually incorporated into official ACL2 releases.

Patch files

We have fixed bugs in the handling of flet expressions, one of which had the capability of rendering ACL2 unsound. Thanks to Sol Swords for his help in identifying these problems. To read more and download the patch file, which includes installation instructions, visit:

http://www.cs.utexas.edu/users/moore/acl2/v3-4/new/flet-patch/index.html

Performance Comparisons

The various cases below correspond to runs of the ACL2 regression suite (distributed and workshop books) for ACL2 executables built on different platforms, as indicated. In each case below, the first number, User time in seconds, is by far the best one to use for comparisons (as opposed to System time or Elapsed time). Not shown here are successful runs on several other platforms: Lispworks 4.4.6 on 32-bit Ubuntu Linux; CMU Common Lisp 18d on Sun/Solaris (SunOS 5.9); CCL 1.2 (1.2-r9918M-trunk DarwinPPC32) and SBCL 1.0.2 on a PowerPC Mac; and GCL 2.6.7 and SBCL 1.0.13 on Windows/MinGW.

All statistics shown below are for running make regression on 8-core machines. The option -j 8 was used (i.e., up to 8 parallel jobs), so again, the first number in each case (marked with "u"), User seconds, is more relevant than the rest. Each regression run was on a 2.2 GHz AMD Opteron (tm) Processor 850 running Ubuntu Linux. One such machine was used for the 32-bit OS runs; another for 64-bit OS runs. NOTE: The 64-bit runs skipped the directory books/clause-processors/SULFA/, which accounts for about 4 or 5 minutes of User time; so the GCL penalty for 64-bit linux may be greater than appears below.

32-bit OS runs

64-bit OS runs

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.