ACL2 Version 6.2 News

ACL2 sources availability between releases
VSTTE 2012 Competition
ACL2 Books Repository
Performance Comparisons

ACL2 sources availability between releases

ACL2 sources are now available between releases, as described in this announcement.

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 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 Mac OS X and preliminary testing on Windows. 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 -j 8

Note: We ran a few tests using CLISP 2.49 as well, but skipped most of the regression because CLISP is several times slower than others.

CCL Version 1.9-dev-r15542M-trunk:

24985.841u 674.910s 57:06.64 748.8%	0+0k 237144+1460040io 260pf+0w

Lispworks Version 6.1.1:

25168.656u 408.197s 56:53.80 749.2%	0+0k 496+1560208io 0pf+0w

Gnu Common Lisp (GCL) Version 2.6.8pre (built 6/6/2013), 1048576 maximum pages
(Note: The book workshops/2013/greve-slind/defung/defung-test.cert failed to certify; we did not manage to reproduce the error. Expected certification time for that book would be a little over a minute.)
```
26795.358u 1006.302s 1:01:16.35 756.2%	0+0k 126744+3873728io 0pf+0w
```

SBCL Version 1.1.7:

30741.697u 525.460s 1:09:16.65 752.2%	0+0k 1336+1824696io 0pf+0w

Allegro CL Version 9.0:

31942.420u 455.268s 1:12:30.33 744.7%	0+0k 6000+1665504io 0pf+0w

CMU Common Lisp (CMUCL) snapshot-2013-05-9-gb3b0725 (20D Unicode):

73109.697u 441.955s 2:40:07.95 765.5%	0+0k 209840+1918456io 159pf+0w

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

Note that unlike the times above, the time just below is for the regression suite for the HONS version of ACL2, i.e., ACL2(h). We show only the CCL time, since that is currently the recommended Lisp for ACL2(h), though some testing was done on other Lisps as well. The increase in CCL time over the time shown above is due, at least in part, to running some extra tests specific to ACL2(h).