ACL2 Version 2.9 Installation Guide

NOTE: When updates are made to these instructions, they are announced on the ACL2 home page under the link "Recent changes to this page".

Table of Contents

UPDATES
REQUIREMENTS
- Obtaining Common Lisp
- Performance comparisons
OBTAINING AND INSTALLING ACL2
USING ACL2
MISCELLANEOUS INFORMATION

UPDATES

From time to time, we provide so-called incremental releases of ACL2. These tend to be significantly improved (fewer bugs, more and enhanced features) over previous releases.

See the Incremental Releases section of the ACL2 Version 2.9 News page for incremental releases.

REQUIREMENTS

ACL2 works on Unix/Linux, Macintosh, and some Windows operating systems (at least including Windows 98, Windows 2000, and Windows XP). It can be built on top of any of the following Common Lisps:

GCL
Allegro Common Lisp
CMU Common Lisp
CLisp
OpenMCL
MCL
Lispworks

Obtaining Common Lisp

ACL2 runs on top of most or all of the major Common Lisp implementations. These are enumerated below, with links. Often we put timing comparisons between different lisps in the ACL2 News.

Obtaining GCL

Gnu Common Lisp (GCL) has probably been the most commonly-used platform for ACL2, certainly among non-commercial Lisps. IMPORTANT: Here we are referring to the non-ANSI version (sometimes called the "CLtL1 version") of GCL. It is probably impossible to build ACL2 with ANSI GCL as of December 2005, but recent GCL advances suggest that this may be possible soon.

Debian package. You do not need to fetch GCL if you download the binary Debian package for ACL2. Thanks to Camm Maguire for maintaining this package.

GCL may be fetched from http://www.gnu.org/software/gcl/. If that site goes down, you may be able to find useful information from the GCL Temporary Distribution Site. GCL maintainer Camm Maguire suggests the following, in order of preference (most to least):

apt-get -q install gcl gcl-doc if running Debian
Download and install the prebuilt binaries otherwise (if available for your platform)
Download the latest (stable) source tarball and build yourself otherwise
Download the latest (stable) cvs branch and build yourself

As of December 2005, the latest recommended version is 2.6.7, and the latest development version is 2.7.0. But see below for suggestions for building GCL on a Macintosh running OS X.

You may obtain recent CVS versions by executing the following commands if you have CVS installed on your system, which will retrieve the latest development/unstable cvs sources by default.

export CVS_RSH=ssh [or, if using csh: setenv CVS_RSH ssh]
cvs -d:ext:anoncvs@subversions.gnu.org:/cvsroot/gcl co gcl

If you happen to know a particular version of GCL that you wish to obtain, perhaps by following GCL mailing lists, you can replace the commands above by commands such as the following.

export CVS_RSH=ssh [or, if using csh: setenv CVS_RSH ssh]
cvs -d:ext:anoncvs@subversions.gnu.org:/cvsroot/gcl co -r Version_x_y_z -d gcl-x.y.z gcl

Macintosh. Robert Krug has provided instructions for building GCL on Mac OS X, which we include here (very slightly modified, in part with help from Camm Maguire) in case others find them helpful.

The normal build process for GCL on Mac OS X assumes that
you have installed fink on your Mac.  (If you do not know
what this is, don't worry; you probably don't have it or
want it.)  Here we give instructions that have worked for
building GCL on OS X without fink.

   A. Obtain recent sources (there is a problem, e.g., with
      gcl-2.6.7).  For example, you can do the following:

      export CVSROOT=:pserver:anonymous@cvs.sv.gnu.org:/sources/gcl
      cvs -z9 -q co -d gcl-2.6.8pre -r Version_2_6_8pre gcl

      At some point you may be able to obtain GCL from
      ftp://ftp.gnu/org/, cd gnu, cd gcl, get
      gcl-2.6.8.tar.gz, tar xfz gcl-2.6.8.tar.gz)

   B. Make sure that /usr/local/bin in in your PATH; if not, run:
      PATH="$PATH:/usr/local/bin"

   C. cd <gcl directory>

   D. You now need to patch file h/powerpc-macosx.defs (this might not be
      necessary starting with GCL 2.6.8):

      Replace the line:
      LIBS := `echo $(LIBS) | sed -e 's/-lncurses/ /'` /sw/lib/libintl.dylib
      With:
      LIBS := `echo $(LIBS) | sed -e 's/-lncurses/ /'` /usr/local/lib/libintl.dylib

   E. Configure and start to build gcl:
      ./configure
      make

   F. Install gcl:
      sudo make install

Obtaining Allegro Common Lisp

Allegro Common Lisp is probably the most commonly-used commercial platform for ACL2. You may be able to obtain a trial version from its web site, http://www.franz.com/.

Obtaining CMU Common Lisp

CMU Common Lisp (sometimes called CMUCL) is a non-commercial Common Lisp implementation, available from http://www.cons.org/cmucl/.

Obtaining CLISP

CLISP is a non-commercial Common Lisp implementation, available from http://clisp.cons.org/.

Obtaining OpenMCL

OpenMCL, a free Common Lisp implementation that runs on Macintosh OS X, is available from http://openmcl.clozure.com/.

Obtaining MCL

Macintosh Common Lisp (MCL), a commercial Lisp for the Macintosh, is available from http://www.digitool.com/.

Obtaining Lispworks

Lispworks is a commercial Common Lisp available from http://www.lispworks.com/.

Lispworks note. We initially encountered a problem in getting ACL2 to run under LIspworks 4.2.0. The Lispworks folks provided a patch and suggested that we make the following announcement.

Users with LispWorks4.2.7 should ask us at lisp-support@xanalys.com for the transform-if-node patch. It will be helpful if they quote (Lisp Support Call #11372) when doing so. Also, they must send a bug form generated from their LispWorks image: instructions at http://www.lispworks.com/support/bug-report.html.

Performance comparisons

Please go to the ACL2 home page and follow the link "Recent changes to this page" to see recent performance numbers.

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.9. We will call this directory dir. For example, dir might be /home/jones/acl2/v2-9.

NOTE: If you intend to obtain an incremental release (e.g. 2.9.3 as opposed to 2.9), please see the ACL2 News for instructions. Otherwise, continue reading here.

Begin by clicking on one of the following links.

Shortcuts
Obtaining the Sources: Unix and Linux
Obtaining the Sources: Other than Unix and Linux Systems

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:

Pre-built Binary Distributions

Visit the "Recent changes to this page" link on the ACL2 home page to see if there are other shortcuts available.

Debian GNU Linux
For Linux (especially Debian GNU Linux), you can download the Debian package for Linux. Thanks to Camm Maguire for maintaining this package, and for pointing out that as Debian packages are simply ar and tar archives, they can be unpacked on any linux system, and who says: If someone is running Debian, all they want to do is 'apt-get install acl2', doing likewise for any optional add-on package they wish as well, e.g. emacs, infix, etc.
You can fetch the above package for a linux system other than Debian and unpack it as follows. First, connect to the directory under which you install ACL2 versions and download the .deb file there. Then submit these commands (changing "2.9.3-7" and "i386" as appropriate).
```
mkdir acl2_2.9.3-7
cd acl2_2.9.3-7
mv ../acl2_2.9.3-7_i386.deb .
ar x acl2_2.9.3-7_i386.deb
tar xvfz data.tar.gz
```
This will create subdirectory usr/. Edit usr/bin/acl2 by replacing "/usr" with the full pathname for "usr".
Alternatively, you can use the program alien to convert the .deb file to .rpm format. Of course, with the method shown above or with alien, you will not have the benefit of package maintenance.
Windows Installer
From time to time, a Windows binary release ("Windows Installer") is made available. Jared Davis has made one available here.

Obtaining the Sources: Unix and Linux

For a Unix or Linux system, obtain the sources and place them in directory dir as follows.

Save acl2.tar.gz on directory dir. (You can run md5sum and compare with acl2.tar.gz.md5sum if you wish to verify the transmission.)
Execute the following four Unix commands. (Note: Gnu tar is preferred, as there have been some problems with long file names when using tar provided by SunOS. You may want to use the -i option, "tar xpvfi acl2.tar", if you have problems with other than Gnu tar. You can see if you have Gnu tar by running "tar -v".)

cd dir
gunzip acl2.tar.gz
tar xpvf acl2.tar
rm acl2.tar

Now proceed to Creating An Executable Image.

Obtaining the Sources: Other than Unix and Linux Systems

For a non-Unix (and non-Linux) system, obtain the sources and place them in directory dir as follows.

[Note for Macintosh users: You may want to look at the sections "Dealing with Unix linebreaks" and (MCL only) "Memory" in file mcl-acl2-startup.lisp.]

[Note for Windows systems: 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. For example, djtarnt.exe from ftp://ftp.gnu.org/gnu/windows/emacs/utilities/i386/djtarnt.exe can be used as follows:

djtarnt.exe -x acl2.tar.gz

Then again, acl2.tar.gz contains files in Unix format, hence if you encounter problems, fetch the files individually. WARNING: At least one user experienced CR/LF issues when using WinZIP, so you may want to avoid WinZIP.]

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-9/acl2-sources. You may link to our ftp sources directory by clicking here.

[Note: You may need to use text mode, not binary mode, for example if you use Fetch on a Macintosh.]

You will find that pub/moore/acl2/v2-9/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.

Tip for Windows users: We have received the suggestion that people untarring with winzip should probably turn off smart cr/lf conversion.

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 take a short cut by downloading an ACL2 image, in which case you can skip ahead to Summary of Distribution. Otherwise you should click on one of the links just below. 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.

PLEASE NOTE: The available memory for ACL2 is determined by the underlying Common Lisp executable. If you need more memory, refer to your Common Lisp's instructions for building an executable.

Building an Executable Image on a Unix or Linux System
Building an Executable Image on Other than Unix and Linux Systems
Running Without Building an Executable Image

Short Cut: Pre-Built ACL2 Images

The ftp site ftp://ftp.cs.utexas.edu:/pub/moore/acl2/v2-9/images/README.html contains links to ACL2 executables and packages. Each .md5sum file was created using md5sum. We may add additional links from time to time.

Note that the Debian images may work with other Linux systems as well.

Now proceed to Using ACL2.

Building an Executable Image on a Unix or Linux System

We assume you have obtained ACL2 and placed it in directory dir, as described above. If you downloaded a pre-built ACL2 image, 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, which can be obtained as explained above.

This will create executable saved_acl2 in the acl2-sources directory.

The time taken to carry out this process depends on the host processor but may be only a few minutes for a fast processor. 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 on Unix and Linux systems we have tested. See the file acl2-sources/GNUmakefile for further details. If this make command does not work for you, please see the instructions for non-Unix/Linux systems below.

You can now skip to Using ACL2.

Building an Executable Image on Other than Unix and Linux Systems

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.

See also Building an Executable Image on Some Particular Systems, in case you want to skip directly to the instructions in one of its subtopics.

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/").

Remove file nsaved_acl2 if it exists.
Start up Common Lisp in the acl2-sources directory and submit the following sequence of commands.
```
  ; Compile
  (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.
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:
```
  ; Initialization, first pass
  (load "init.lsp")
  (in-package "ACL2")
  (load-acl2)
  (initialize-acl2)
```
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 saying that it is impossible to finish because a certain file was compiled during the processing, thus dirtying the image yet again. (If however the attempt ends with an error during compilation of file TMP1.lisp, see the first troubleshooting tip below.)
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:
```
  ; Initialization, second pass
  (load "init.lsp")
  (in-package "ACL2")
  (save-acl2 (quote (initialize-acl2))
             "saved_acl2")
```
You have now saved an image. Exit Lisp now. Subsequent steps will put the image in the right place.
Remove osaved_acl2 if it exists.
IF saved_acl2 and saved_acl2.dxl both exist THEN:
- move saved_acl2.dxl to osaved_acl2.dxl
- move saved_acl2 to osaved_acl2 and edit osaved_acl2, changing saved_acl2.dxl (at end of line) to osaved_acl2.dxl
ELSE IF saved_acl2 exists THEN:
- move saved_acl2 to osaved_acl2
Move nsaved_acl2 to saved_acl2.
For Allegro Common Lisp, Versions 5.0 and later, nsaved_acl2.dxl should exist; move it to saved_acl2.dxl
Make sure saved_acl2 is executable.

Building an Executable Image on Some Particular Systems

Subtopics of this section are as follows.

Special Case: Building an Executable Image on Mac OS X using GCL
Special Case: Building an Executable Image on a Windows System using GCL
Instructions from Jared Davis for building ACL2 on Windows using mingw

How to build/install ACL2 on GCL on Mac OS X

See the directions above for bulding GCL on Mac OS X. Then follow the usual installation instructions to obtain the ACL2 sources and build an executable image on a Unix/Linux system.

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

You may be able to download a pre-built ACL2 image for GCL/Windows. In that case you can probably skip the rest of this section. Alternatively, skip this section and read Instructions from Jared Davis for building ACL2 on Windows using mingw.

Otherwise here are steps to follow.

FIRST get GCL running on your Windows system using ONE of the following two options. Note that GCL can be unhappy with spaces in filenames, so you should probably save the GCL distribution to a directory whose path is free of spaces.
- OR, obtain GCL for Windows systems from ftp://ftp.gnu.org/gnu/gcl/ or as explained above. You may wish to pick a .zip file from the cvs/ subdirectory (containing pre-releases) that has "mingw32" in the name.
- OR ELSE, perhaps you can build GCL on your Windows system from the sources. The mingw tools and the cygnus bash shell have been used to build distributed GCL executables.
SECOND, create an appropriate GCL batch file. When we tried running the script gclm/bin/gclm.bat that came with gcl-cvs-20021014-mingw32 from the above ftp site, a separate window popped up, and with an error. Many ACL2 users prefer running in an emacs shell buffer. (We obtained emacs for Windows from ftp://ftp.gnu.org/gnu/windows/emacs/21.2/emacs-21.2-fullbin-i386.tar.gz.) The following modification of gclm.bat seemed to solve the problem (your pathnames may vary).
```
@
% do not delete this line %
@ECHO off
set cwd=%cd%
path C:\gcl\gclm\mingw\bin;%PATH%
C:\gcl\gclm\lib\gcl-2.6.1\unixport\saved_gcl.exe -dir C:/gcl/gclm/lib/gcl-2.6.1/unixport/ -libdir  C:/gcl/gclm/lib/gcl-2.6.1/ -eval "(setq si::*allow-gzipped-file* t)" %1 %2 %3 %4 %5 %6 %7 %8 %9
```
THIRD, follow the instructions for non-Unix/Linux systems above, though the resulting file may be called saved_acl2.exe rather than saved_acl2.
FINALLY, create a file acl2.bat as explained in ftp://ftp.cs.utexas.edu/pub/moore/acl2/v2-9/images/README.html.

We hope that the above simply works. If you experience problems, the following hints may help.

TROUBLESHOOTING:

We tried building ACL2 on Windows XP on top of GCL, our attempt broke at the end of the "Initialization, first pass" step, while compiling TMP1.lisp. That was easily remedied by starting up a fresh GCL session and invoking (compile-file "TMP1.lisp") before proceeding to the next step.
Yishai Feldman has provided some nice instructions at http://www.faculty.idc.ac.il/yishai/reasoning/win-install.htm, some of which we have tried to incorporate here. A useful point made there is that when you want to quit ACL2, use :good-bye (or (good-bye) which works even in raw Lisp). Or you can use (user::bye) in raw Lisp. The point is: Avoid control-c control-d, even thought that often works fine in emacs under Unix/Linux.
If the above batch file does not work for some reason, an alternate approach may be to set environment variables. You may be able to add to the PATH variable gcl-dir\gcc\bin, where gcl-dir is the directory where GCL is installed. To get to the place to set environment variables, you might be able to go to the control panel, under system, under advanced. Alternately, you might be able to get there by opening My Computer and right-clicking to get to Properties, then selecting the Advanced tab. At one time, when GCL/Windows was release as Maxima, Pete Manolios suggested adding the system variable LD_LIBRARY_PATH with the value "maxima-dir\gcc\i386-mingw32msvc\include"; this may or may not be necessary for your GCL installation (and the path would of course likely be different).

Instructions from Jared Davis for building ACL2 on Windows using mingw

We thank Jared Davis for providing the following instructions for Version_2.8, which we include verbatim and expect apply to future versions.

	      Building ACL2 on Windows from Scratch
   _____________________________________________________________

   Note: The disk space requirements are large.  Not including
   emacs, I had about 275 MB taken up by msys/mingw32/gcl/acl2
   during the build process.  You can probably use much less
   space by removing files after you use them, but I didn't
   bother to do that.

   Here are the steps I took:

   Downloaded emacs 21.3 full distribution and installed
   Downloaded msys 1.10.10, installed to c:\acl2
   Downloaded mingw 3.1.0-1, installed to c:\acl2\mingw
   Downloaded gcl 2.5.3, extracted to c:\acl2\mingw
   Downloaded acl2 2.8, extracted to c:\acl2\sources



   Compiling gcl:

     in msys:

       cd /acl2/ming2/gcl-2.5.3
       ./configure
       make
       make install



   Compiling acl2:

     copy "etags.exe" to /mingw/bin.  you can find this program
     in your emacs folder, under "bin".

     in msys:

       cd /sources
       make



   Certifying ACL2 books:
   This took 111 minutes on my Athlon 2500+

     in msys:

       cd /sources

       mv nsaved_acl2.gcl.exe saved_acl2.exe

       vim books/Makefile-generic, remove "nice" from this line:
	   ACL2=time nice ../../saved_acl2

       make certify-books ACL2=/sources/saved_acl2.exe

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 a pre-built ACL2 image, then 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)

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)
  (initialize-acl2)

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
  GNUmakefile ; For Unix/Linux make.
  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)
images/    ; Some gzip'd tar'd executables; see images/README
split/     ; The result of splitting up acl2.tar.gz; see split/README

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 30 to 60 megabytes depending 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/GNUmakefile 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, which is a good idea anyhow; this is our next topic. On a Unix/Linux system, you can also certify just a small but useful subset of the books in a few minutes by executing, in directory dir/acl2-sources:

make certify-books-short

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/Linux. 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. Failure is indicated by the presence of **CERTIFICATION FAILED** in the log.

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/Linux 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/Linux users: we do not provide non-Unix/Linux 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/Linux makefile (GNUmakefile) 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 1100 pages or more than 2 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, a search button (near the top of the page), 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. (Macintosh users using MacOS 9 and earlier may, however, find filenames being truncated and hence will want to avoid the local documentation.)

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.

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 (1.2 MB) version is available. It prints as a book of about 1000 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. When 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.

Note, however, that you may find it more convenient to view the documentation in a web browser (starting at doc/HTML/acl2-doc.html) or in Emacs info (starting at doc/EMACS/acl2-doc-emacs.info).

This completes the installation of ACL2 Version 2.9. 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 Linux Slackware v3.0:

Fetch GCL v2.2 plus fixes. Install it using the standard makefile. The GCL v1.0 binaries that come with Slackware were not built correctly (it fails to load compiled *.o files).
Add the following lines at the end of acl2_sources/init.lsp
```
#+gcl
(setq COMPILER::*SPLIT-FILES* 100000)
```
This way the lisp compiler splits large C source files in files of about 100K. Without this line, some systems do not have enough memory to compile the C files. (We saw this problem arise on a machine with 16Mb of actual memory plus 16Mb of virtual memory.)
Install ACL2 using the standard makefile (GNUmakefile). It requires about 25Mb of free disk space (besides space for source files).

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.

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

This will create executable saved_acl2r in the dir/acl2-sources directory (notice the trailing ~code>r in the executable filename).

Finally, to certify books under directory dir/acl2-sources/books/nonstd/with ACL2(r), stand in thedir/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.

acl2-help@lists.cc.utexas.edu
ACL2 help list, for questions about using ACL2.
acl2@lists.cc.utexas.edu
General ACL2 list for users and others interested in ACL2.

You may subscribe to or unsubscribe from these lists 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 for use (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

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.