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.
The statistics below correspond to runs of make -j 8
regression using
the community
books, skipping
directory 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
SBCL for demos/meta-wf-guarantee-example.lisp: some
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
filename.
39355.836u 767.207s 1:35:59.05 696.6% 0+0k 785456+3738096io 249pf+0w
51821.243u 802.366s 2:06:39.76 692.4% 0+0k 684320+3420112io 331pf+0w
54146.808u 701.288s 2:07:11.58 718.6% 0+0k 1009656+3433664io 171pf+0w
61113.144u 1762.886s 2:26:35.30 714.8% 0+0k 1648824+8492056io 575pf+0w
66894.365u 984.830s 2:40:10.43 706.3% 0+0k 603976+3438512io 103pf+0w
137600.352u 988.074s 5:24:10.41 712.5% 0+0k 614992+3938888io 180pf+0w