Obtaining and Installing ACL2

[Back to main page of Installation Guide.]

NOTES

You may want to skip this page and simply use the instructions for "Easy Install for Unix-like Systems".
For information about getting started with ACL2, see the "Start Here" documentation page.

TABLE OF CONTENTS

Pre-built Binary Distributions
Obtaining the Sources and Community Books
Creating or Obtaining an Executable Image
Running Without Building an Executable Image
Summary of ACL2 System Distribution
GitHub Distributions

ACL2 is more than just the executable image. In particular, it comes with a user's manual, and the system is distributed with libraries developed by the ACL2 community, the community books. Start here and we will take you through the whole process of obtaining and installing ACL2.

First, create a directory under which to store ACL2 Version 8.6. We will call this directory dir. For example, dir might be /home/jones/acl2/.

Pre-built Binary Distributions

See the ACL2 documentation page on pre-built binary distributions, which includes discussion of ACL2s binaries, Windows, MacPorts for Mac OS X, and Debian GNU Linux.

Obtaining the Sources and Community Books

Here is how to obtain the sources and community books and place them in a directory, dir.

(First, a note for Windows users only: we suggest that you obtain a Unix-like environment or, at least, download a utility such as djtarnt.exe to use with the -x option on gzipped tarfiles. 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.)

Save acl2-8.6.tar.gz on directory dir.

Execute the following four Unix commands to obtain the ACL2 system and community books. (Note: Gnu tar is preferred, as there have been some problems with long file names when using at least one other tar program. You may want to use the -i option, "tar xpvfi 8.6.tar", if you have problems with other than Gnu tar. You can see if you have Gnu tar by running "tar -v".) The resulting tarball and its extracted directory may consist of 230M+ bytes and 1100M+ bytes, respectively. Additional space is required to build an executable image, for example, 170M+ bytes if you use CCL and 230M bytes if you use SBCL; and considerably more will be required to certify books.

cd dir
tar xfz acl2-8.6.tar.gz
rm acl2-8.6.tar.gz
cd acl2-8.6

Note: You can also fetch the latest GitHub distribution the ACL2 system and the community books, as shown below.

git clone https://github.com/acl2/acl2

Moreover, you can contribute books by joining the GitHub project.

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. However, you may be able to take a short cut by downloading an ACL2 image, in which case you can skip ahead to the page on Using ACL2. 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).

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-like System
Building an Executable Image on Other than a Unix-like System
Running Without Building an Executable Image

Short Cut: Pre-Built ACL2 Images

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

Now proceed to Using ACL2.

Building an Executable Image on a Unix-like 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. Change directory to dir as above and execute

cd
acl2-8.6

make LISP=xxx

where xxx is the command to run your local Common Lisp.

By default, if no LISP=xxx is specified, LISP=ccl is used. On our hosts, ccl is the name of Clozure Common Lisp (CCL), which can be obtained as explained in the Requirements document.

This will create executable saved_acl2 in the acl2-8.6 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 a couple hundred megabytes or so.

This make works for the Common Lisp implementations listed in Requirements document on systems we have tested. See the file acl2-8.6/GNUmakefile for further details. If this make command does not work for you, please see the instructions below for other than Unix-like systems.

You can now skip to Using ACL2.

Building an Executable Image on Other than a Unix-like System

Next we describe how to create a binary image containing ACL2 without using the `make' utility. 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-8.6 directory; please change to that directory before continuing.

Remove file nsaved_acl2 if it exists.

Start up Common Lisp in the acl2-8.6 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-8.6 subdirectory. Here we assume that executables have extension .dxl, but this will depend on your host Lisp and operating system.

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 change to the acl2-8.6 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 change to your acl2-8.6 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 some Common Lisps, a file nsaved_acl2.suffix is created for some suffix. Move it to: saved_acl2.suffix

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.

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. See also additional information about ACL2 on Windows. Or, you may be able to download a pre-built ACL2 image for Windows instead of reading this section.

Otherwise here are steps to follow. (These are quite old and may have bugs. Please report any bugs to the Matt KaufmannACL2 implementors.)

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.2\unixport\saved_gcl.exe -dir C:/gcl/gclm/lib/gcl-2.6.2/unixport/ -libdir  C:/gcl/gclm/lib/gcl-2.6.2/ -eval "(setq si::*allow-gzipped-file* t)" %1 %2 %3 %4 %5 %6 %7 %8 %9
```
THIRD, follow the instructions for other than Unix-like 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/v8-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-like systems.
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 released 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-like systems 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-like systems or other platforms. (If you downloaded a pre-built ACL2 image, then you may skip this section.) Change to subdirectory acl2-8.6 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, execute the following forms after starting up Common Lisp in subdirectory acl2-8.6 of dir. This may take a minute or two (which is another reason to consider installing an executable image as described above, using `make' if possible).

  (load "init.lisp")
  (in-package "ACL2")
  (load-acl2)
  (initialize-acl2)
  (lp) ; enter the ACL2 read-eval-print loop

Now proceed to read more about Using ACL2.

Summary of ACL2 System Distribution

This section, which is optional, discusses how to browse a distribution that includes ACL2 only, without the community books.

We discuss above how to obtain a gzipped tarfile that contains both the ACL2 sources and the community books. Below we describe the ACL2 distribution only (without the community books) from the University of Texas at Austin. Its files are available by exploring the distrib/ directory on this website or by obtaining a gzipped tarfile, acl2.tar.gz, which extracts to the contents of distrib/acl2-sources/, which in turn contains the ACL2 source files as well as the following (and a few others not mentioned here).

  LICENSE       ; ACL2 license file
  GNUmakefile   ; For GNU make
  TAGS          ; Handy for looking at source files with emacs
  TAGS-acl2-doc ; Handy for finding code in books, e.g., with the acl2-doc browser
  bin/          ; Contains an executable script, bin/acl2, which invokes ACL2
  doc/          ; ACL2 documentation
  emacs/        ; Some helpful emacs utilities
  installation/ ; Installation instructions (start with installation.html)

Also available are the following.

ACL2 customization files: These ACL2 customization files can be useful for certifying books, for example with ACL2(p).
images/: Some gzip'd tar'd executables; see images/Readme.html
split/: The result of splitting up acl2.tar.gz

GitHub Distributions

We strongly recommend that ACL2 users update their local copies of the system and community books at each ACL2 release. While that should suffice for many ACL2 users, nevertheless for those who prefer to obtain the latest developments, the ACL2 source code and community books have been made available between ACL2 releases, by way of revision control using git. See the project website for more information.

[Back to Installation Guide.]