Table of Contents
Please let us know if there is
other information that you would find of use in this guide.
Building ACL2 may fail with 32-bit SBCL because of insufficient heap memory. Harsh Raju Chamarthi points out that a fix is to run SBCL with an increased heap size limit, like this:
make LISP="He adds that this issue occurred while building ACL2 4.0 with SBCL v1.0.40 on linux, and the default heap size for SBCL on a standard 32-bit linux is 512MB, while for SBCL (64-bit executable) on a 64-bit linux, the default is usually 8GB.
/sbcl --core /sbcl.core --dynamic-space-size 1024"
REALfor information about this extension and how to build it, and a warning about its experimental nature.
If you care to use ACL2(r), we strongly suggest that you first
download the non-standard analysis community books (gzipped tar file) from
project website, and save to the
books/ subdirectory of your copy of the ACL2 distribution, say,
dir/acl2-sources/books/. Then extract to create
tar xvfz nonstd-6.0.tar.gz
Next build an executable image and certify books. First, connect to your
/acl2-sources/ directory and execute
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-sources directory (notice the trailing
r in the executable filename).
Finally, to certify books under directory
with ACL2(r), stand in the
/acl2-sources/ directory and execute the
make regression-nonstd ACL2=dir/acl2-sources/saved_acl2r
Finally, please report bugs in ACL2 to
Matt Kaufmann and J Strother Moore.
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.
[Back to Installation Guide.]