ACL2 Version 8.2 Performance Comparisons

ACL2 Version 8.2 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.) The listing is alphabetized by host Common Lisp

NOTE. Although these comparisons are intended to give some sense of how these Lisps perform, they are far from definitive, mostly because they don't certify exactly the same books. For example 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 than that, however, the same books were certified with CCL and SBCL. Another reason to be cautious in using these statistics is that compilation in some Lisps could slow down the regression but produce better code (e.g., for running proofs or user applications). Here are links to files that each contain a list of all books certified using the host Lisp indicated in its filename.

number of books    filename

   5374            certs-allegro.txt
   5574            certs-ccl.txt
   5273            certs-gcl.txt
   5393            certs-lispworks.txt
   5573            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.