Table of Contents
Please let us know if there is
other information that you would find of use in this guide.
Building ACL2 with SBCL may require the use
--dynamic-space-size. This is explained in the
section on Obtaining
REALfor information about this extension and how to build it, and a warning about its experimental nature.
If you care to use ACL2(r), you will need to build an executable image
and you will probably want to certify books. First, connect to your
/acl2-8.4/ directory and
make large-acl2r LISP=xxx
where xxx is the command to run your local Common Lisp.
By default, if no
LISP=xxx is specified,
LISP=ccl is used. On our hosts,
ccl is the name of
Clozure Common Lisp (CCL), which can be obtained as explained in the Requirements document.
This will create executable
saved_acl2r in the
/acl2-8.4 directory (notice the final
r in the executable filename).
Finally, you can certify books under directory
dir/acl2-8.4/books/nonstd/ with ACL2(r) in the usual
way; for example, see the documentation topic for
Finally, please report bugs in ACL2 to
This version of ACL2 is a descendent of ACL2 Version 1.9, Copyright (C) 1997 Computational Logic, Inc.
This program is free software; you can redistribute it and/or modify it under the terms of the LICENSE file distributed with ACL2.
This program is distributed in the hope that it will be useful, but WITHOUT ANY WARRANTY; without even the implied warranty of MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the LICENSE for more details.
Matt Kaufmann (Kaufmann@cs.utexas.edu)
J Strother Moore (Moore@cs.utexas.edu)
Department of Computer Sciences
University of Texas at Austin
Austin, TX 78712-1188 U.S.A.
For more information on copyright, licensing, and authorship, see the
Although releases are best obtained according to the installation instructions by fetching a gzipped tar file from GitHub containing ACL2 Version 8.4 and the corresponding Community Books, here we note that the git commit hash for Version 8.4 of ACL2 on github is: