ACL2 Version 7.1 News

Table of Contents

ACL2 sources availability between releases

ACL2 sources are available between releases at the ACL2 GitHub Repository.

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 -j 8 regression using the community books, skipping directory books/clause-processors/SULFA/, for ACL2 executables built on Linux platforms as indicated. Each regression was run on Ubuntu Linux. (Not shown are results of successful testing with CCL and SBCL on Mac OS 10.10.3.)

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

These times are for the regression suite based on ACL2, which is the default (hons enabled) build. That suite has several books not in the "classic" ACL2(c) regression suite (see next section). Also note that the set of books certified with ACL2 was a bit smaller for GCL than the others (as per books/GNUmakefile).

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

Note: We ran the "basic" suite (acl2-sources/GNUmakefile target certify-books-short) using CLISP 2.49 as well, but skipped the full "all" regression because CLISP is historically several times slower than others.