ACL2 Version 6.4 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. (We used the acl2-books svn branch 6.4/, revision 2407.) Each regression was run on Ubuntu Linux. (Not shown are results of successful testing of ACL2 and ACL2(h) built on CCL version 15835 on Mac OS 10.6.8.) NOTE: The set of tests depends somewhat on the host Lisp (as per books/GNUmakefile). However the statistics may still be useful in comparing performance.

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 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.

CCL Version 1.10-dev-r15915M-trunk:

29011.385u 436.583s 1:13:44.07 665.6%	0+0k 203344+1697136io 195pf+0w

Gnu Common Lisp (GCL)
Note: With GCL ANSI (just below) and CCL (just above), 3340 books were certified; with GCL CLtL1, 3290 books were certified (others were skipped).

Version 2.6.10 ANSI, 33554429 maximum pages:
```
30532.736u 990.629s 1:15:18.68 697.6%	0+0k 456640+6702576io 343pf+0w
```
Version 2.6.10 CLtL1, 33554429 maximum pages:
```
27973.428u 926.121s 1:10:32.72 682.7%	0+0k 147232+6452512io 3pf+0w
```
Version 2.6.8 CLtL1, 1048576 maximum pages:
```
29047.643u 1003.590s 1:13:03.65 685.5%	0+0k 140784+4191944io 0pf+0w
```

Lispworks Version 6.1.1:

30206.303u 446.915s 1:14:00.63 690.2%	0+0k 0+1821480io 0pf+0w

SBCL Version 1.1.11:

36287.511u 616.754s 1:30:37.44 678.7%	0+0k 896+2156896io 0pf+0w

Allegro CL Version 9.0:

38155.240u 514.900s 1:36:39.16 666.8%	0+0k 185720+1945928io 142pf+0w

CMU Common Lisp (CMUCL) snapshot-2013-06 (20D Unicode)

99391.327u 522.484s 4:08:01.38 671.4%	0+0k 213616+2225896io 179pf+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 times just below are for the regression suite based on the the HONS version of ACL2, i.e., ACL2(h). Note that CCL is highly optimized for ACL2(h), so it is the recommended host Lisp for ACL2(h). The increases in times over the time shown above are due, at least in part (and especially for CCL), to running some extra tests specific to ACL2(h).