Miscellaneous Information

[Back to main page of Installation Guide.]

Table of Contents

Please let us know if there is other information that you would find of use in this guide.


Problems

If you are having problems using the make utility, be sure that you are using GNU make.

Reasoning about the Real Numbers

ACL2 supports rational numbers but not real numbers. However, starting with Version 2.5, a variant of ACL2 called "ACL2(r)" supports the real numbers by way of non-standard analysis. ACL2(r) was conceived and first implemented by Ruben Gamboa in his Ph.D. dissertation work, supervised by Bob Boyer with active participation by Matt Kaufmann. See the documentation topic REAL for 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 dir/acl2-sources/ directory and execute

cd acl2-sources
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 dir/acl2-sources directory (notice the trailing r in the executable filename).

Finally, to certify books under directory dir/acl2-sources/books/nonstd/ with ACL2(r), stand in the dir/acl2-sources/ directory and execute the following command. 

make regression-nonstd ACL2=dir/acl2-sources/saved_acl2r


Links and Mailing Lists

There are two mailing lists for ACL2 users. You can post messages to these lists only if you are a member. You may subscribe to or unsubscribe from these lists, or view their archives, at:

You can search the ACL2 documentation, workshops, and publications online from http://www.cs.utexas.edu/users/moore/acl2/admin/forms/search.html.

Finally, please report bugs in ACL2 to acl2-bugs@utlists.utexas.edu.


Export/Re-Export Limitations

ACL2 may be exported to any countries except those subject to embargoes under various laws administered by the Office of Foreign Assets Control ("OFAC") of the U. S. Department of the Treasury.

License and Copyright

ACL2 Version 3.6.1 -- A Computational Logic for Applicative Common Lisp
Copyright (C) 2009 University of Texas at Austin

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.]