ACL2 Version 2.6 Installation Guide

Table of Contents



REQUIREMENTS

ACL2 Version 2.6 Copyright (C) 2001 University of Texas at Austin. ACL2 is licensed under the terms of the GNU General Public License. See below for details.

ACL2 works on the Unix (and some variants, including Linux), Macintosh, and some Windows operating systems (at the least, Windows 98 and Windows 2000). It is built on top of any of the following Common Lisps: Allegro, GCL (Gnu Common Lisp) [or, AKCL], CLISP, CMU Lisp, and MCL (Macintosh Common Lisp), and has also been built in the past on Lispworks and Lucid.

(Old remark, potentially obsolete for most users:) We have successfully run a small but nontrivial test suite on a Sparc 2 with 16 megabytes of main memory, but performance appears better with more memory. For more on this, see Problems.


OBTAINING AND INSTALLING ACL2

ACL2 is more than just the executable image. You should obtain the standard books and a local copy of the documentation. Start here and we will take you through the whole process of obtaining and installing ACL2. First, create a directory in which to store ACL2 Version 2.6. We will call this directory dir. For example, dir might be /home/jones/acl2/v2-6. Begin by clicking on one of the following links.

The sources come with books that you may find helpful in your proof development and programming with ACL2. Two collections of books are not included with the sources:



Obtaining the Sources: Unix (and Linux)

For a Unix or Linux system, obtain the sources and place them in directory dir as follows. Now proceed to Creating An Executable Image.

Obtaining the Sources: Non-Unix Systems

For a non-Unix (and non-Linux) system, obtain the sources and place them in directory dir as follows. Note: You may be able to download a gunzip/tar utility from the internet for your system, in which case you may not need to fetch individual files as discussed below; then again, acl2.tar.gz contains files in Unix format, hence if you encounter problems, fetch the files individually.

Create a subdirectory of dir named acl2-sources.

Open an ftp connection to ftp.cs.utexas.edu by anonymous login and ftp to the local acl2-sources subdirectory all of the files and directories in and below the ftp directory pub/moore/acl2/v2-6/acl2-sources. You may link to our ftp sources directory by clicking here.

You will find that pub/moore/acl2/v2-6/acl2-sources contains many files, subdirectories, sub-subdirectories, etc. We mean for you to copy over to your local connected directory the entire structure of files and subdirectories. Thus, when this ftp operation is done, your local connected directory should have a subdirectory named acl2-sources and it should contain (at some level) everything obtained by the ftp. Your local acl2-sources subdirectory will now look exactly as though you had obtained our acl2.tar.gz and done the gunzip, tar and rm steps of the Unix instructions.

Now proceed to Creating An Executable Image.


Creating An Executable Image

The next step is to create an executable image. The common approach is to build that image from the sources you have already obtained. However, you may be able to download an executable image. If you downloaded an image, then you can skip ahead to Using ACL2. Otherwise you should click on one of the following links. Choose the last option if you are using a Common Lisp on which you cannot save an image (e.g., a trial version of Allegro Common Lisp). Exception: If you are using Macintosh Common Lisp (MCL), then follow the instructions in source file mcl-acl2-startup.lisp to complete the installation, and then proceed to Using ACL2.

Short Cuts: Downloading Executable Images

You may follow one of these links now if you are running on the indicated system and want to take a short cut by downloading an image:

Short Cut: Solaris 7 Sparc running GNU Common Lisp

We assume you have obtained ACL2 and placed it in directory dir, as described above.

Short Cut: Debian GNU/Linux running GNU Common Lisp

Note: This short cut may apply to other Linux systems as well, not just Debian GNU/Linux. For example, a short test indicated that this image works with Red Hat Linux release 7.1.

We assume you have obtained ACL2 and placed it in directory dir, as described above.



Short Cut: Solaris 7 Sparc running CLISP

We assume you have obtained ACL2 and placed it in directory dir, as described above.



Short Cut: Debian GNU/Linux running CLISP

Note: This short cut may apply to other Linux systems as well.

We assume you have obtained ACL2 and placed it in directory dir, as described above.



Short Cut: Solaris 7 Sparc running CMUCL

We assume you have obtained ACL2 and placed it in directory dir, as described above.



Short Cut: Redhat 7.2 Linux running CMUCL

Note: This short cut may apply to other Linux systems as well. Thanks to Michael "Bogo" Bogomolny for building this image for CMUCL 2.4.17.

We assume you have obtained ACL2 and placed it in directory dir, as described above.



Building an Executable Image on a Unix System

We assume you have obtained ACL2 and placed it in directory dir, as described above. If you downloaded an image (see instructions above), you may skip this section. Otherwise, connect to dir as above and execute

cd acl2-sources
make 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. You can fetch GCL without fee from ftp://ftp.ma.utexas.edu/pub/gcl/ (which has the latest GCL version as of 12/01 that we know of, GCL 2.4.0, which we have built on Debian Gnu Linux), ftp://prep.ai.mit.edu/pub/gnu/gcl/, or from mirror sites listed at http://www.gnu.org/order/ftp.html.
Linux notes. We have successfully built ACL2 under Debian Gnu Linux with GCL 2.3 and 2.4.0, and have been told by GCL author Bill Schelter that GCL 2.3.6 works with Redhat 6.1 and 6.2. One user has found GCL 2.3 (as opposed to 2.3.6) satisfactory with Redhat 6.1, while another experienced rare problems with Redhat 6.2 using GCL 2.3 that went away with GCL 2.3.6.

The time taken to carry out this process depends on the host processor but may be only several minutes for a fast processor (by June 2000 standards). The size of the resulting binary image is dependent on which Lisp was used, but it may be in the vicinity of 17 megabytes.

This make works for the Common Lisps listed in Requirements above. It may only work on Sun Sparcs and 486/66 PCs, for all we know about the portability of Unix Makefile code. See the file acl2-sources/Makefile for further details. If this make command does not work for you, please see the instructions for non-Unix systems below.

You can now skip to Using ACL2.



Building an Executable Image on a Non-Unix System

Next we describe how to create a suitable binary image containing ACL2. If you are running Macintosh Common Lisp (MCL), then see the source file mcl-acl2-startup.lisp and then skip to Using ACL2. If you are using a trial version of Allegro Common Lisp, then you may not be able to save an image. In that case, skip to Running Without Building an Executable Image.

If you are building under Windows using GCL, you may want to proceed directly to instructions for building on Windows using GCL.

Otherwise, proceed as follows.

Your Common Lisp should be one of those listed in Requirements above. Filenames below should default to the dir/acl2-sources directory, e.g., for GCL, connect to dir/acl2-sources before invoking GCL or, after entering GCL, do (si::chdir "dir/acl2-sources/").

  1. Remove file nsaved_acl2 if it exists.

  2. Start up Common Lisp in the acl2-sources directory and submit the following sequence of commands. 
      (load "init.lsp")
  (in-package "ACL2")
  (compile-acl2)
    The commands above will compile the ACL2 sources and create compiled object files on your acl2-sources subdirectory.

  3. Now exit your Common Lisp and invoke a fresh copy of it (mainly to avoid saving an image with the garbage created by the compilation process). Again arrange to connect to the acl2-sources subdirectory. In the fresh Lisp type: 
      (load "init.lsp")
  (in-package "ACL2")
  (load-acl2)
  (initialize-acl2 (quote include-book) *acl2-pass-2-files* t t)
    This will load the new object files in the Lisp image and bootstrap ACL2 by reading and processing the source files. But the attempt at initialization will end in an error! The message will say that it is impossible to finish because a certain file was compiled during the processing, thus dirtying the image yet again.

  4. So now exit your Common Lisp and invoke a fresh copy of it (again arranging to connect to your acl2-sources subdirectory). Then, in the fresh Lisp type: 
      (load "init.lsp")
  (in-package "ACL2")
  (save-acl2 (quote (initialize-acl2 (quote include-book) *acl2-pass-2-files* t))
             "saved_acl2")
    You have now saved an image. Exit Lisp now. Subsequent steps will put the image in the right place.

  5. Remove osaved_acl2 if it exists.

  6. IF saved_acl2 and saved_acl2.dxl both exist THEN: ELSE IF saved_acl2 exists THEN:

  7. Move nsaved_acl2 to saved_acl2.

  8. For Allegro Common Lisp, Versions 5.0 and later, nsaved_acl2.dxl should exist; move it to saved_acl2.dxl

  9. Make sure saved_acl2 is executable.


Special Case: Building an Executable Image on a Windows System using GCL

These instructions are slightly edited from instructions that were graciously provided by Pete Manolios. These instructions are for Windows 2000; one may have to make adjustments for other Windows systems.

1. Download maxima from http://www.ma.utexas.edu/users/wfs/maxima-download/maxima55l-setup.exe. This is an executable file that installs maxima. Run the executable which will result in maxima being installed in the directory of your choosing, say maxima-dir.

2. In the control panel, under system, under advanced, under environment variables:

3. Now follow the ACL2 instructions for building an executable image on a non-unix system until you get to step 2. Copy maxima-dir\src\saved_maxima to the acl2-sources directory and move "init.lsp" to "initialize.lisp". Start maxima-dir\src\saved_maxima. The prompt should be "MAXIMA>>". Do the following: 

	:q  ;  To get the prompt "MAXIMA>"
	(in-package "lisp")
	(load "acl2.lisp")
	(in-package "ACL2")
	(compile-acl2)
The commands above will compile the ACL2 sources and create compiled object files on your acl2-sources subdirectory.

4. Now exit gcl (i.e., saved_maxima) and invoke a fresh copy of it (mainly to avoid saving an image with the garbage created by the compilation process). In the fresh Lisp type: 

	:q  
	(in-package "lisp")
	(load "initialize.lisp")
	(in-package "ACL2")
	(load-acl2)
	(initialize-acl2 (quote include-book) *acl2-pass-2-files* t t)
This will load the new object files in the Lisp image and bootstrap ACL2 by reading and processing the source files. But the attempt at initialization will end in an error! The message will say that it is impossible to finish because a certain file was compiled during the processing, thus dirtying the image yet again.

5. So now exit gcl, invoke a fresh copy, and type: 

	:q  
	(in-package "lisp")
	(load "initialize.lisp")
	(in-package "ACL2")
	(save-acl2 (quote (initialize-acl2 (quote include-book) *acl2-pass-2-files* t))
		   "saved_acl2")
You have now saved an image. Exit Lisp now. Subsequent steps will put the image in the right place.

6. Move nsaved_acl2 to saved_acl2, move initialize.lsp to init.lsp. Remove saved_maxima from the acl2-sources directory and add ";acl2-sources" to the PATH variable.

[End of Pete's instructions.]

Bill Schelter has added the following information.

The maxima which one can download actually contains src/saved_maxima.exe which is a maxima executable but that contains GCL.

One way of getting it to start as plain GCL is to add to a file init.lsp in the directory where you start maxima 

  (setq SYSTEM::*TOP-LEVEL-HOOK* nil)
then it will start with the usual lisp prompt. The init.lsp delivered with maxima also has the path set to add the path for "gcc" so that the compiler works.

You can build gcl from scratch using the mingw tools, and the cygnus bash shell. That is how that one was built.


Running Without Building an Executable Image

The most convenient way to use ACL2 is first to install an executable image as described above for Unix/Linux and other platforms. However, in some cases this is not possible, for example if you are using a trial version of Allegro Common Lisp. In that case you should follow the steps below each time you want to start up ACL2.

We assume you have obtained ACL2 and placed it in directory dir, as described above for Unix/Linux or other platforms. If you downloaded an image (see instructions above), then you have an image and hence you may skip this section. Otherwise, connect to subdirectory acl2-sources of dir, start up your Common Lisp, and compile by executing the following forms. This sequence of steps need only be performed once. 

  (load "init.lsp")
  (in-package "ACL2")
  (compile-acl2 nil)
Now each time you want to use ACL2, you need only execute the following forms after starting up Common Lisp in subdirectory acl2-sources of dir. 
  (load "init.lsp")
  (in-package "ACL2")
  (load-acl2 nil)
  (initialize-acl2 (quote include-book) *acl2-pass-2-files* nil)
Note. The resulting process includes the ACL2 documentation, and hence will probably be considerably larger (perhaps twice the size) than the result of running an executable image created as described above.

Now proceed to read more about Using ACL2.


Summary of Distribution

The distribution includes the following. A list of all files in acl2-sources may be found in the file all-files.txt in that directory. 
README.html; This file
acl2-sources/
  LICENSE  ; GNU General Public License
  Makefile ; For Unix make.  See README.
  TAGS     ; Handy for looking at source files with emacs
  *.lisp   ; ACL2 source files
  all-files.txt   ; List of all files in this directory and subdirectories
  books/   ; Examples, potentially useful in others' proofs.  See books/README.html.
  doc/     ; ACL2 documentation in various formats
  emacs/   ; Miscellaneous emacs and file utilities, especially emacs-acl2.el
  init.lsp ; Useful for building the system
  interface/
    emacs/ ; Support for ACL2 "proof trees".  See interface/emacs/README.doc.
    infix/ ; ACL2 infix printer by Mike Smith.  See interface/infix/README.
  saved/   ; Empty directory for backing up copies during make; not important
acl2.tar.gz; gzip'd tar file containing all of acl2-sources/ (see below)
acl2.tar.gz.SUM ; result of our running sum acl2.tar.gz
images/    ; Some gzip'd tar'd executables
split/     ; The result of splitting up acl2.tar.gz

The entire acl2.tar.gz is roughly 4.6 megabytes, which expands out to roughly 19 megabytes. Additional space is required to build an image, perhaps 17 megabytes (though this depends on the Lisp), and to certify books.


Saving Space

For those really pressed for space, we note that it is not necessary to fetch the whole acl2.tar.gz file in order to build acl2. That file includes more than just the ACL2 sources proper. It suffices, for building ACL2, via the instructions above, to fetch only the acl2-sources/*.lisp files, which take up `only' about 5 megabytes, together with the files acl2-sources/Makefile and acl2-sources/init.lsp.

USING ACL2

Here we begin with a discussion of how to invoke ACL2 interactively. We then discuss testing as well as the certification of ACL2 books that come with the distribution. We conclude with a discussion of the documentation.

Invoking ACL2

At this point, dir has a subdirectory called acl2-sources. The sources and perhaps an executable image are located on that subdirectory. However, if you have not saved an image but instead use the directions above for Running Without Building an Executable Image, skip to When ACL2 Starts Up below.

The executable image is called acl2-sources/saved_acl2. You can invoke ACL2 by running that image, e.g.,

mycomputer% dir/acl2-sources/saved_acl2

If on a Unix/Linux system, then to make it easy to invoke ACL2 by typing a short command, e.g.,

mycomputer% acl2

you may want to install an executable file on your path, e.g., /usr/local/bin/acl2, containing the following two lines:

#!/bin/csh -f
dir/acl2-sources/saved_acl2


Note: A carriage return in the file after the last line above is important!


When ACL2 Starts Up

When you invoke ACL2, you should see the host Common Lisp print a header concerning the ACL2 version, license and copyright.

Some hosts then automatically enter the ACL2 ``command loop,'' an ACL2 read-eval-print loop with the prompt: 

ACL2 !>
Other hosts will leave you in Common Lisp's read-eval-print loop. If yours is one of the latter, evaluate the Common Lisp expression (ACL2::LP) or simply (LP) if the current package is "ACL2".

Once in the ACL2 command loop, you can type an ACL2 term, typically followed by ``return'' or ``enter,'' and ACL2 will evaluate the term, print its value, and prompt you for another one. Below are three simple interactions: 

ACL2 !>t
T
ACL2 !>'abc
ABC
ACL2 !>(+ 2 2)
4

To get out of the ACL2 command loop, type the :q command. This returns you to the host Common Lisp. We sometimes call this ``raw Lisp.'' You may re-enter the command loop with (LP) as above.

Note that when you are in raw Lisp you can overwrite or destroy ACL2 by executing inappropriate Common Lisp expressions. All bets are off once you've exited our loop. That said, many users do it. For example, you might exit our loop, activate some debugging or trace features in raw Lisp, and then reenter our loop. While developing proofs or tracking down problems, this is reasonable behavior.

Now you are ready to test your image.


Testing ACL2

An easy way to test the theorem prover is to type the following term to the ACL2 command loop: 

:mini-proveall
This will cause a moderately long sequence of commands to be processed, each of which is first printed out as though you had typed it. Each will print some text, generally a proof of some conjecture. None should fail.

A more elaborate test is to certify the ``books'' that come with the distribution.


Certifying ACL2 Books

The ``books'' that come with the distribution have been contributed mainly by users and are on the subdirectory acl2-sources/books. See acl2-sources/books/README.html for information. The general topic of books is discussed thoroughly in the ACL2 documentation; see the BOOKS node in the documentation tree.

Books should be ``certified'' before they are used. We do not distribute certificates with our books, mainly because certification produces compiled code specific to the host. You should certify the books locally as a test of your ACL2 image.

It is easy to re-certify all the distributed books in Unix. We recommend you do this. If you have entered ACL2, exit to the operating system, e.g., by control-d in many systems.

While connected to dir/acl2-sources, execute 

make certify-books
This will generate minimal output to the screen and will probably take an hour or two. To remove the files thus created, invoke: 
make clean-books

The certify-books target does not cause workshop books to be certified. If you want to certify those books as well, you will first need to download the gzipped tar file to the books/ directory, and then gunzip and extract it. You can certify all the books, including books for the workshops (including those from the 1999 workshop as described in the (hardbound) book Computer-Aided Reasoning: ACL2 Case Studies), using the command: 

make regression

By default, certification uses the image dir/acl2-sources/saved_acl2. You may specify any ACL2 image, as long as it is either a command on your Unix path or an absolute file name, for example as follows. 

make certify-books ACL2=my-acl2

make regression ACL2=/u/smith/projects/acl2/saved_acl2

We apologize to non-Unix users: we do not provide non-Unix instructions for recertifying the distributed books. The certification methods provided by the authors of the books vary greatly and we codified them in the Unix Makefile used above. Most subdirectories of acl2-sources/books contain either a README file or a certify.lsp file. Users who wish to certify one of these books and who cannot figure out (from these scant clues) what to type to ACL2 should not hesitate to contact the authors.

Next proceed to the section on Documentation.


Documentation

ACL2's documentation is a hypertext document that, if printed in book form, is about 800 pages or about 1.5 megabytes of text. Its hypertext character makes it far more pleasing to read with an interactive browser. The documentation is available in four formats: HTML, Texinfo, Postscript and ACL2 documentation strings. All of this material is copyrighted by the University of Texas at Austin and is derived under the GNU General Public License from material copyrighted by Computational Logic, Inc.

Two Web-based guided tours of ACL2 are available from the home page noted below. If you are already familiar with Nqthm, you might find it useful to look at the documentation node NQTHM-TO-ACL2. Another useful documentation topic for beginning ACL2 users is the node TUTORIAL.

HTML

The ACL2 Home Page is

http://www.cs.utexas.edu/users/moore/acl2/index.html

The home page provides a selected bibliography, guided tours of the system, and the complete hypertext documentation tree.

Once you have installed ACL2, the HTML form of the documentation is available locally as dir/acl2-sources/doc/HTML/acl2-doc.html.

We urge you to browse your local copy of the documentation rather than our Web copy, simply to reduce Web traffic and the demand on our server.

Emacs Info

This is a very convenient format for accessing the ACL2 documentation from within Emacs. In Emacs, invoke 

meta-x info
and then, if you are unfamiliar with Info, type 
control-h m
to see a list of commands available. In particular, type

g (dir/acl2-sources/doc/EMACS/acl2-doc-emacs.info)TOP

to enter the ACL2 documentation. Alternatively, your system administrator can add an ACL2 node to the top-level Info menu. The appropriate entry might read:

* ACL2 i.j: (dir/acl2-sources/doc/EMACS/acl2-doc-emacs).
          Documentation for ACL2 version i.j.

If you are using Lucid Emacs instead of Gnu Emacs, you will find it more aesthetic to use

dir/acl2-sources/doc/LEMACS/acl2-doc-lemacs.info

instead of

dir/acl2-sources/doc/EMACS/acl2-doc-emacs.info.

Note: The Emacs Info and Postscript versions of our documentation were created using the file acl2-sources/doc/texinfo.tex which is copyrighted by the Free Software Foundation, Inc. (See that file for copyright and license information.)

Users new to emacs may find it helpful to load into emacs the file dir/acl2-sources/emacs/emacs-acl2.el. Utilities offered by this file are documented near the top of the file.

Postscript

The Postscript version of the documentation is not included in our normal distribution because it is so much less useful than the hyper-text versions. But a gzipped Postscript (1MB) version is available. It prints as a book of almost 900 pages and contains a Table of Contents and an index to all documented topics.

ACL2 Documentation Strings

The ACL2 system has facilities for browsing the documentation. However this requires that the documentation be stored as strings in the Lisp image. To save space, the images mentioned so far in this document do not contain resident documentation strings. To build such an image on a Unix system, invoke

make large LISP=xxx

while connected to the acl2-sources directory. The xxx above should be replaced by the name of 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.) This will create dir/acl2-sources/saved_acl2 (note that this is the same name previously used for the image without documentation strings). The new image may be 30 megabytes in size and take several minutes to build on a fast (in June 2000) machine. For non-Unix systems, the ``large'' image can be built in your local Common Lisp by following instructions given above and then saving the image created by the final initialize-acl2 form to an executable binary file.

Once you have an image of ACL2 containing documentation strings, and you are in the ACL2 command loop, you may query the documentation on a given topic by typing the command

:doc topic

where topic is the Lisp symbol naming the topic you want to learn about. To learn more about the on-line documentation, type :help and then return.

This completes the installation of ACL2 Version 2.6. You may wish to return to the Table of Contents.


MISCELLANEOUS INFORMATION

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

Problems

If you have difficulties with ftp time outs after establishing an ftp connection, please try logging in again using a dash (-) as the first character of your password -- this will turn off the continuation messages that may be confusing your ftp client. If that doesn't solve your problems, and you have encountered problems ftping the long file acl2.tar.gz because your get times out, an alternative is to get all of the many files in the directory split/, each of which matches the pattern split-acl2.tar.gz* (e.g., using an `mget' command). Once you have got all these files, concatenate them together in alphabetic order, e.g., with the command 
cat split-acl2.tar.gz* > acl2.tar.gz

If you are using Version 3.2.0 of Lispworks, there is probably a bug in the definition of logeqv. Harlequin has sent us a patch; if anyone asks us for it, we will ask Harlequin if we may forward their patch.

If you are running on GCL or AKCL on a machine with only 16 megabytes of RAM, it may be a good idea to have a file ~/acl2-init.lsp containing the following form, which will help to keep the ACL2 process small as you are running it: 

(setq acl2::*acl2-allocation-alist* nil).
In one test several years ago, we found the following times (minutes:seconds) using a Sparc 2. 
31:42   64 megabytes main memory
33:37   64 megabytes main memory, using the SETQ form above
63:52   16 megabytes main memory
43:09   16 megabytes main memory, using the SETQ form above

If you are running Linux Slackware v3.0:

Thanks to Vanderlei Moraes Rodrigues for the Slackware notes.


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.

Useful Addresses

There are mailing lists for ACL2. You may subscribe or unsubscribe at 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 (e.g., how to retrieve archive messages). If you need further assistance, please send a message to acl2-request@lists.cc.utexas.edu.

You can retrieve archive files or search the archives using a web interface from http://www.cs.utexas.edu/users/moore/acl2/admin/forms/archive.html.

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@lists.cc.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 2.6 -- A Computational Logic for Applicative Common Lisp
Copyright (C) 2001 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.