ACL2 Version 8.0 News

Table of Contents

Bug Fixes

Here is a link to a patch file that fixes an ACL2 8.0 soundness bug in the automatic functional instantiation that can be applied for a :termination-theorem lemma instance. Thanks to Eric Smith for sending an example to illustrate this bug, for suggesting its cause, and for permission to include that example in a comment in the ACL2 sources definition of the constant, *non-instantiable-primitives*.

This bug is fixed in the ACL2 GitHub repository.

Changelogs

The "changelogs" for ACL2 are in the release-notes topics of the manuals. In particular, there are release notes for Version 8.0.

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 GitHub repository allows contributions ACL2 books (input files), and also provides between-release updates.

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: some time ago, 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.