ACL2 Version 4.1 News

Table of Contents

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 various cases below correspond to runs of the ACL2 regression suite (distributed and workshop books) for ACL2 executables built on different platforms, as indicated. Not shown are results of testing on Windows and Mac OS X or of running with safety 3 using CCL.

Statistics shown below are for running make regression. Each 32-bit Linux regression reported below was run with make option -j 8 on an 8-core 2.2 GHz AMD Opteron (tm) Processor 850 running Ubuntu Linux. Each 64-bit Linux regression reported below was run with make option -j 24 on a 2.6GHz machine with four processors, each a Six-Core AMD Opteron(tm) Processor 8435. Also, the 64-bit runs skipped directory books/clause-processors/SULFA/. So comparisons between a 32-bit run and 64-bit run are ill-advised.

32-bit Linux runs using make -j 8

64-bit Linux runs using make -j 24

Note: We ran regression using CLISP 2.41 as well, but without the workshops/ books. The user time alone was 66869.515u.

ACL2 Course Materials

At some point, perhaps "ACL2 Course Materials" may be a top-level link on the ACL2 home page. For now, we provide some links.