ACL2 Version 6.0 News

Table of Contents

VSTTE 2012 Competition

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

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 ACL2_JOBS=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. Not shown are results of testing on Windows and Mac OS X. Each regression was run on Ubuntu Linux.

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

Note: We ran regression using CLISP 2.44.1 as well, but without the centaur/ or workshops/ books. The wall clock time was close to 3 hours, far exceeding all the times just below even though those include certification of the above books.

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

Note that unlike the times above, the times just below are for the regression suite for the HONS version of ACL2, i.e., ACL2(h).

32-bit ACL2 Linux runs on 2.8 GHz 4-core Intel(R) Xeon(R) with Hyper-Threading, using make ACL2_JOBS=8

ACL2 Course Materials

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