Installing ACL2

Pre-requisite software

ACL2 requires GNU make. On Linux and OS X, at least, GNU make is the default make. On other systems, like FreeBSD and OmniOS (a Solaris descendant), it isn't. On those systems, you may need to invoke GNU make as gmake. The bash shell and perl are also required by the build process.

So, to sum up: ensure that you have GNU make, bash, and perl.

Getting ACL2 sources

ACL2 source code is available on GitHub?.

A potential hazard is that git clone won't change anything if the acl2 directory already exists. If you want to be sure that you're building from a newly downloaded copy, rm -rf acl2 before trying to clone. If you're trying to ensure that an existing copy of acl2 sources are up-to-date, git pull is probably preferable.

Generally speaking, the combination of "git pull" and cleaning the books (e.g., using 'make' target regression-everything-fresh or starting with 'make' target moreclean) should be sufficient to stay out of trouble from stale files.

cd /usr/local/src
git clone
cd acl2
gmake LISP=ccl64 # or whatever

cd books
gmake ACL2=/usr/local/src/acl2/saved_acl2 -j 6 basic
gmake ACL2=/data/rme/acl2/saved_acl2 MAKE=gmake -j 8 regression-everything-fresh

Note that one of the tests relies on ccl:contrib;huebner;advice-profiler; so grab that if needed with

svn co svn://

N.B.: you will typically not need to do this. If you get ccl in the "official" way by doing

svn co

you will get the contrib/ directory without any further action on your part.

Doing make regression-everything-fresh should run a fairly extensive set of tests and create ~4500 .cert files. There are some additional documented options that force some tests that depend on things installed via quicklisp. The "-fresh" variant removes the .cert files before doing make regression-everything.

A typical invocation is something like cd acl2;time nice make -j 4 make regression-everything-fresh >some logfile. Without the "nice", it can use all of the core, swap, and cycles that it can. -j 8 might have completed sooner but renders my machine even more unusable than -j 4 does. ymmv. Running make with the default "basic" target may be useful to ensure that things are set up as expected.

2015-11-20T19:56:31Z gb: one test - whose name I can't remember - takes a a very long time. It uses automatically generated code and creates functions that contain thousands of function calls. it has caused CCL to run out of labels and other finite resources, and puts a very heavy load on the machine. It fails on "sbcl", and is excluded from the test suite by makeology. (The file in question is books/demos/meta-wf-guarantee-example.lisp)

ACL2 Documentation

Last modified 4 years ago Last modified on Dec 3, 2015, 8:38:23 PM