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
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
This bug is fixed in the ACL2 GitHub repository.
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 are available between releases at the ACL2 GitHub Repository.
A team of four ACL2 users entered the VSTTE 2012 competition. For information, including the team's solution, visit this link.
The ACL2 GitHub repository allows contributions ACL2 books (input files), and also provides between-release updates.
The statistics below correspond to runs of
make -j 8
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
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
52895.680u 981.032s 2:13:49.06 671.0% 0+0k 1940784+4274640io 371pf+0w
60247.416u 663.276s 2:19:45.19 726.4% 0+0k 1952576+4115608io 303pf+0w
64702.940u 837.356s 2:43:13.54 669.2% 0+0k 1658368+3957824io 393pf+0w
76578.024u 1310.776s 2:56:49.30 734.1% 0+0k 4140728+9893384io 1412pf+0w
78489.468u 824.092s 3:03:31.18 720.3% 0+0k 2289800+4207056io 445pf+0w