Table of Contents
Please let us know if there is
other information that you would find of use in this guide.
makeutility, be sure that you are using GNU
REALfor information about this extension and how to build it, and a warning about its experimental nature.
if you care to use ACL2(r), first
download the non-standard analysis books (gzipped tar file) to the
books/ subdirectory of your copy of the ACL2 distribution, say,
dir/acl2-sources/books/. Then run:
tar xvfz nonstd.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=gcl is used. On our hosts,
gcl is the name of
GNU Common Lisp, 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
http://www.cs.utexas.edu/users/moore/acl2/admin/forms/email.html. You should receive a confirmation of the request a short time later, along with instructions for use (e.g., how to retrieve archive messages). If you need further assistance, please send a message to
You can retrieve archive files or search the archives using a web interface
You can search the ACL2 documentation, workshops, and publications online from
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 GNU General Public License as published by the Free Software Foundation; either version 2 of the License, or (at your option) any later version.
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 GNU General Public License for more details.
You should have received a copy of the GNU General Public License along with this program; if not, write to the Free Software Foundation, Inc., 675 Mass Ave, Cambridge, MA 02139, USA.
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.]