ACL2 Version 8.1 Performance Comparisons

ACL2 Version 8.1 Performance Comparisons

The information below is based on runs of make -j 8 regression using the community books, skipping directory books/clause-processors/SULFA/, with Glucose installed. Each regression was run on Ubuntu Linux, on 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.13.6.)

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. There are other examples. Here are links to files that each contain a list of all books certified using the host Lisp indicated in its filename; note that exactly the same books were certified with CCL and SBCL except for the one mentioned above.

number of books filename

5094 certs-allegro.txt
5288 certs-ccl.txt
5004 certs-gcl.txt
5115 certs-lispworks.txt
5287 certs-sbcl.txt

Note that CMU Common Lisp (CMUCL) is not currently supported for building and running ACL2, as explained here.

Please bear in mind the discrepancy in sets of books certified, as noted above, when comparing the times listed below.