ACL2 Version 7.2 News

Table of Contents

Changelogs

 The "changelogs" for ACL2 are in the release-notes topics of the manuals. In particular, there are release notes for Version 7.2, which in turn links to the release notes for the corresponding community books.

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/, and not using Glucose or Quicklisp. Each regression was run on Ubuntu Linux a 3.5 GHz 4-core Intel(R) Xeon(R) with Hyper-Threading. (Not shown are results of successful testing with CCL on Mac OS 10.10.5.)

NOTE. Although these comparisons are intended to give some sense of how these Lisps perform, they are far from definitive. For example, compilation in some Lisps could slow down the regression but produce better code (e.g., for running proofs or user applications). Also, note that certification is skipped in SBCL for demos/meta-wf-guarantee-example.lisp: we aborted certification after 75 minutes, while in CCL for example, certification took about 3 minutes. Other examples: the book books/tools/oracle-time-tests.lisp has special, less computationally intensive code for CMUCL. Here is a link to a directory for which each file contains a list of all books certified using the host Lisp indicated in its filename.