ACL2 Version 6.5 News
Table of Contents
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
and acl2.org),
skipping directory books/clause-processors/SULFA/, for
ACL2 executables built on Linux platforms as indicated. (We used the
acl2-books svn branch 6.5/, revision 2915.) Each regression was run
on Ubuntu Linux. (Not shown are results of successful testing of ACL2
and ACL2(h) built on CCL version 16150 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-r16149M-trunk:
31087.814u 440.787s 1:11:51.66 731.2% 0+0k 15896+1844064io 0pf+0w
- Gnu Common Lisp (GCL) Version 2.6.11 CLtL1, 33554429 maximum pages:
33198.662u 914.961s 1:17:25.49 734.3% 0+0k 326256+3456920io 221pf+0w
- Gnu Common Lisp (GCL) Version 2.6.10 CLtL1, 33554429 maximum pages:
33936.832u 1024.308s 1:18:35.42 741.4% 0+0k 448896+6657376io 326pf+0w
- Lispworks Version 6.1.1:
30889.574u 446.011s 1:10:49.43 737.4% 0+0k 10848+1928208io 0pf+0w
- SBCL Version 1.2.1
33311.609u 628.851s 1:16:43.16 737.3% 0+0k 389584+2264272io 341pf+0w
Allegro CL Version 9.0:
41572.366u 507.071s 1:35:21.14 735.5% 0+0k 856+2041848io 0pf+0w
CMU Common Lisp (CMUCL) snapshot-2014-06 (20E Unicode)
92840.790u 524.040s 3:26:42.54 752.7% 0+0k 66288+2363416io 0pf+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 HONS
version of ACL2, i.e., ACL2(h). Note that CCL is highly
optimized for ACL2(h), thus, it is the recommended host Lisp for
ACL2(h). The increases in times over those without HONS, shown above,
may be due (at least in part) to having certified about 15 extra books
(for each host Lisp) with ACL2(h).
- CCL Version 1.10-dev-r16149M-trunk:
32084.173u 1239.477s 1:15:10.79 738.7% 0+0k 280+1809256io 0pf+0w
- Lispworks Version 6.1.1:
33678.032u 530.529s 1:17:07.52 739.2% 0+0k 224648+1809632io 135pf+0w
- SBCL Version 1.2.1:
40082.793u 963.128s 1:41:04.91 676.7% 0+0k 427344+2137048io 281pf+0w
- Allegro CL Version 9.0:
43481.637u 571.515s 1:38:50.00 742.8% 0+0k 6640+1906160io 0pf+0w
- Gnu Common Lisp (GCL) Version 2.6.10 ANSI, 33554429 maximum pages:
44530.638u 1750.345s 1:44:28.64 738.2% 0+0k 483704+27155576io 88pf+0w
- CMU Common Lisp (CMUCL) snapshot-2014-06 (20E Unicode)
96872.898u 575.651s 3:34:29.04 757.2% 0+0k 236656+2230000io 154pf+0w