ACL2 Version 6.3 News

Table of Contents

ACL2 sources availability between releases

ACL2 sources are now available between releases, as described in
this announcement.

VSTTE 2012 Competition

A team of four ACL2 users entered the VSTTE 2012 competition. For information, including the team's solution, visit this

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.

Performance Comparisons

The statistics below correspond to runs of make -j 8 regression using community books (available from the acl2-books project website), skipping directory books/clause-processors/SULFA/, for ACL2 executables built on Linux platforms as indicated. (The acl2-books svn revision number is 2093 for the trunk, which was used to create the 6.3 branch as revision 2094.) Each regression was run on Ubuntu Linux.

(Not shown are results of testing with CCL and SBCL on Mac OS 10.6.8 and preliminary testing on Windows. GCL 2.6.8 on Mac OS 10.6.8 also worked fine, except for two failures due to storage exhaustion, workshops/2013/greve-slind/defung/defung-test.cert and centaur/regression/common.cert.)

64-bit ACL2 Linux runs on 3.5 GHz 4-core Intel(R) Xeon(R) with Hyper-Threading, using make -j 8

Note: We ran a few tests using CLISP 2.49 as well, but skipped most of the regression because CLISP is historically several times slower than others.

64-bit ACL2(h) Linux runs on 3.5 GHz 4-core Intel(R) Xeon(R) with Hyper-Threading, using make -j 8

Note that unlike the times above, the times just below are for the regression suite based on the the HONS version of ACL2, i.e., ACL2(h). Note that CCL is highly optimized for ACL2(h), so it is the recommended host Lisp for ACL2(h). The increase in CCL time over the time shown above is due, at least in part, to running some extra tests specific to ACL2(h).