ACL2 Version 6.3 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), skipping
directory books/clause-processors/SULFA/, for ACL2
executables built on Linux platforms as indicated. (The acl2-books
svn revision number is 2093 for the trunk, which was used to create
the 6.3 branch as revision 2094.) Each regression was run on Ubuntu
Linux.
(Not shown are results of testing with CCL and SBCL on Mac OS 10.6.8
and preliminary testing on Windows. GCL 2.6.8 on Mac OS 10.6.8 also
worked fine, except for two failures due to storage exhaustion,
workshops/2013/greve-slind/defung/defung-test.cert
and centaur/regression/common.cert.)
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 historically several times slower than
others.
- CCL Version 1.10-dev-r15915M-trunk:
27521.179u 482.354s 1:13:46.14 632.6% 0+0k 235496+1609880io 219pf+0w
- Lispworks Version 6.1.1:
28944.252u 490.658s 1:16:13.79 643.5% 0+0k 1368+1724248io 0pf+0w
- Gnu Common Lisp (GCL) Version 2.6.10, 16777213 maximum pages:
29080.449u 1063.298s 1:16:41.68 655.0% 0+0k 459048+6701544io 386pf+0w
- Gnu Common Lisp (GCL) Version 2.6.8, 1048576 maximum pages:
30144.603u 1176.089s 1:19:27.64 656.9% 0+0k 484552+4273744io 381pf+0w
- SBCL Version 1.1.11:
34903.029u 647.484s 1:31:43.41 645.9% 0+0k 483344+2009472io 367pf+0w
- Allegro CL Version 9.0:
37261.516u 524.364s 1:41:01.89 623.3% 0+0k 182288+1842848io 174pf+0w
- CMU Common Lisp (CMUCL) snapshot-2013-06 (20D Unicode)
85754.119u 542.633s 3:44:58.30 639.3% 0+0k 211408+2109152io 181pf+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 increase in CCL time over the time shown above is due, at least in
part, to running some extra tests specific to ACL2(h).
- CCL Version 1.9-dev-r15542M-trunk:
30304.497u 1252.206s 1:20:52.69 650.2% 0+0k 976+1641704io 0pf+0w
- Lispworks Version 6.1.1:
31155.139u 564.743s 1:20:23.67 657.5% 0+0k 234496+1656008io 185pf+0w
- SBCL Version 1.1.11:
38724.264u 995.622s 1:39:12.80 667.2% 0+0k 497536+1981528io 355pf+0w
- Allegro CL Version 9.0:
40811.362u 643.864s 1:47:47.80 640.9% 0+0k 5856+1799824io 0pf+0w
- Gnu Common Lisp (GCL) Version 2.6.10pre, 33554429 maximum pages (the default on the machine used):
(Note: This GCL 2.6.10pre was obtained 10/2/2013, git commit e5aa9e95642b60764ffdbe03038a2cf093c90b2d .)
45662.837u 2000.153s 1:57:57.00 673.4% 0+0k 483928+30306392io 112pf+0w
- CMU Common Lisp (CMUCL) snapshot-2013-06 (20D Unicode)
90644.572u 597.781s 3:53:59.35 649.9% 0+0k 824+2022280io 0pf+0w