Obtaining and Installing ACL2

[Back to main page of Installation Guide.]

Table of Contents

Pre-built Binary Distributions
Obtaining the Sources: Unix, Mac OS X, and Linux
Obtaining the Sources: Other than Unix, Mac OS X, and Linux Systems
Creating or Obtaining an Executable Image
Running Without Building an Executable Image
Summary of Distribution
Saving Space

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

NOTE: If you intend to obtain an incremental release (e.g. 2.9.4 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.

Pre-built Binary Distributions
Obtaining the Sources: Unix, Mac OS X, and Linux
Obtaining the Sources: Other than Unix, Mac OS X, and Linux Systems

The sources come with a books subdirectory, in particular books/Readme.html (here for the latest non-incremental release) that you may find helpful in your proof development and programming with ACL2. The following two collections of books are not included with the sources. You can extract them in the books/ subdirectory of your ACL2 distribution; see the discussion on certifying books for information on using them.

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-7" and "i386" as appropriate).
```
mkdir acl2_2.9-7
cd acl2_2.9-7
mv ../acl2_2.9-7_i386.deb .
ar x acl2_2.9-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.
MacPorts for Mac OS X
ACL2 versions are sometimes made available under MacPorts (formerly darwinports) for Mac OS X, courtesy of Greg Wright, who has graciously provided the initial version of the following insructions.
ACL2 can be built on OS X using the MacPorts system. For more information on MacPorts, including instructions on downloading and installing the MacPorts infrastructure, see http://macports.org. One thing to remember is to add MacPorts executable directory (/opt/local/bin by default) to your path.
Once MacPorts is installed, do the following. You can stand in any directory when executing these commands, as the installation is independent of where these commands are run. You can skip the first three if you haven't installed previous versions of MacPorts or DarwinPorts.
```
	   # sudo port clean --all acl2
           # sudo port uninstall acl2 +certify
           # sudo port uninstall acl2 +regression
	   # sudo port install acl2 +certify
```
It's not necessary to obtain a Lisp implementation first, as one is automatically downloaded and built as a dependency of ACL2.
To build the system without certifying books (though you probably will want to certify books, by using the preceding install command), change the install command to:
```
	   # sudo port install acl2
```
To build the system and certify the workshop books in addition to the distributed books, change the install command to the following (but note that this full regression takes a long time, more than 12 hours on a PowerBook G4 800 MHz).
```
	   # sudo port install +regression
```
The default build uses SBCL, which works for both Intel and PPC. If you want to use OpenMCL on PPC, add +openmcl to your install command.
To build ACL2(r) -- Ruben Gamboa's extension of ACL2 for reasoning about the real numbers using non-standard analysis -- use the following command, which will build both ACL2 and ACL2(r) and will certify books for ACL2(r).
```
	   # sudo port install +nonstd
```
Once ACL2 is installed, it can be invoked using 'acl2' at the command prompt. (Use 'acl2r' for ACL2(r) instead.)
More on dealing with old versions (for MacPorts).
If you have an old version around from MacPorts or DarwinPorts, an alternative to uninstall is deactivate. Greg Wright explains as follows:
The only difference between "uninstall" and "deactivate" is that uninstall saves the files in a tarball and deletes the installed files. Deactivate, by contrast, keeps the files in an internal directory and unlinks them from the user-visible directory. You can reactivate by using "port activate", which is faster than a reinstall from the tarball. Of course, only one version of a port may be active at a time.
If an attempt to use uninstall or deactivate reports an error, then you may need to provide a version as suggested by the error message, e.g.:
```
	   # sudo port deactivate acl2 @3.0_1+certify
```
Windows Installer
The Windows Installer for ACL2 includes a Unix environment, pre-certified standard and workshop books, and a copy of Gnu Emacs.

Obtaining the Sources: Unix, Mac OS X, and Linux

For a Unix, Mac OS X, 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 or Obtaining an Executable Image.

Obtaining the Sources: Other than Unix, Mac OS X, and Linux Systems

For a non-Unix (and non-Linux, non-Mac-OS-X) system, obtain the sources and place them in directory dir. The easiest way to do this is to fetch file http://www.cs.utexas.edu/users/moore/acl2/v3-6/new/v3-6-1/acl2.tar.gz, and then extract using an appropriate tar utility. For example, for Windows systems you may be able to download a utility such as djtarnt.exe to be used as follows:

djtarnt.exe -x acl2.tar.gz

WARNING: At least one user experienced CR/LF issues when using WinZIP, but we have received the suggestion that people untarring with that utility should probably turn off smart cr/lf conversion.

You will find that the ACL2 distribution 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 you have completed extracting from acl2.tar.gz, or fetching all files directly is done, your local connected directory should have a subdirectory named acl2-sources under which everything resides.

Now proceed to Creating or Obtaining an Executable Image.

Creating or Obtaining 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. 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).

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, Mac OS X, or Linux System
Building an Executable Image on Other than Unix, Mac OS X,and Linux Systems
Running Without Building an Executable Image

Building an Executable Image on a Unix, Mac OS X, or Linux System

We assume you have obtained ACL2 and placed it in directory dir, as described above. 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 in the Requirements document.

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 document on 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, Mac OS X, and Linux Systems

Next we describe how to create a suitable binary image containing 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 document. 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.lisp")
  (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.lisp")
  (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.lisp")
  (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. For Windows this involves two mini-steps: (a) Remove the "$*" from the saved_acl2 script (because Windows does not understand $*). Consequently, any arguments you pass to ACL2 via the command line will be ignored. (b) Rename saved_acl2 to saved_acl2.bat, for example by executing the following command.

rename saved_acl2 saved_acl2.bat

Building an Executable Image on Some Particular Systems

Subtopics of this section are as follows.

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

If you want to build/install ACL2 on Mac OS X, you may find it easier to do so on top of OpenMCL rather than GCL. Otherwise, see the directions 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 want to skip this section and instead read Instructions from David Rager for building ACL2 on Windows.

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 http://www.cs.utexas.edu/users/moore/acl2/v3-6/distrib/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).

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. 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.lisp")
  (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.lisp")
  (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.lisp; 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.html
split/     ; The result of splitting up acl2.tar.gz; see split/Readme.html

The entire acl2.tar.gz is about 10.5 megabytes, which expands out to about 60 megabytes. Additional space is required to build an image, perhaps 40 to 170 megabytes or more depending on the Lisp, and to certify books.

[Back to Installation Guide.]