ACL2 Version 3.4 Images

Executable Images

Although the executable images below can be used as is, we strongly recommend that you first obtain the ACL2 sources. Then obtain images as explained below. Finally, you can then certify all books by connecting to the acl2-sources/ directory and executing:

make regression ACL2=<your_ACL2_script>

Additional images may appear on this site from time to time.

For the images below you should create executable wrapper scripts such as the ones shown, and you will need to run gunzip on the .gz file that you download.

NOTE: In some cases, you may be better served by downloading or creating a more recent underlying Lisp executable and then building ACL2 from sources (following the installation instructions).

Gzipped Ubuntu Linux GCL 2.6.7 images:
- 32-bit image, gzipped (md5sum file)
- 64-bit image, gzipped (md5sum file)
Here is the wrapper script. Replace ACL2_DIR by your acl2-sources/ directory path. For the 64-bit version, replace ``ubuntu'' with ``ubuntu64''.
```
#!/bin/sh
export ACL2_SYSTEM_BOOKS=ACL2_DIR/books
exec "ACL2_DIR/ubuntu-linux-gcl-saved_acl2.gcl" $*
```

Gzipped CCL 1.2 images for Darwin/Macintosh
Obtain one of the following files, according to whether you have a PowerPC Macintosh or an Intel Macintosh.
- Power PC Mac gzipped tar file
- Intel Mac gzipped tar file
Now extract your file with one of the following two commands (for PowerPC and Intel Mac, respectively), which will create a subdirectory of the same name but without the >.tgz extension.
```
tar xvfz ccl-1.2-darwinppc-acl2.tgz
tar xvfz ccl-1.2-darwinx8664-acl2.tgz
```
The new subdirectory will have one file. Move that file into your acl2-sources/ directory (and then you may delete the empty subdirectory).
Now execute the following commands to create a ccl/ directory for CCL and download CCL Version 1.2. Below, we write CCL_DIR for a directory, such as /Users/joe/ccl-releases, under which you will keep your CCL releases. The last command is shown in two flavors: Pick the first for a PowerPC Mac and the second for an Intel Mac.
```
mkdir CCL_DIR
mkdir CCL_DIR/1.2
cd CCL_DIR/1.2/
# Pick on (PowerPC or Intel):
svn co http://svn.clozure.com/publicsvn/openmcl/release/1.2/darwinppc/ccl
svn co http://svn.clozure.com/publicsvn/openmcl/release/1.2/darwinx8664/ccl
```
Create a wrapper script, say ccl, for invoking CCL, to reside in any directory you choose. Simply modify the script below, appropriately replacing CCL_DIR.
```
#!/bin/sh

export CCL_DEFAULT_DIRECTORY=CCL_DIR/1.2/ccl

CCL_DIR/1.2/ccl/scripts/openmcl $*
```
Next, create wrapper script saved_acl2 in your acl2-sources directory, by modifying the script below, replacing ACL2_DIR by your acl2-sources/ directory path and appropriately replacing CCL_DIR as above.
NOTE! Instructions are shown for a PowerPC Mac. For an Intel Mac, replace dppccl with dx86cl64
```
#!/bin/sh

export CCL_DEFAULT_DIRECTORY="CCL_DIR/1.2/ccl"
exec "CCL_DIR/1.2/ccl/dppccl" -I "ACL2_DIR/saved_acl2.dppccl" -e "(acl2::acl2-default-restart)" $*
```
You'll need to save the above wrapper script as an executable file (chmod +x ccl-saved_acl2).
Now certify books by running
make regression
in your acl2-sources/ directory.

Complete Packages:

The following packages are available for some versions of ACL2. When available, they include everything you need; you do not need to download acl2.tar.gz if you download one of these.

WARNING: Some of these packages might be for old version of ACL2. We recommend that you use the latest version of ACL2 (Version 3.4).

Debian packages. Thanks to Camm Maguire for creating and maintaining the Debian packages for ACL2.
Windows Installers. Thanks to Alex Spiridonov, Jared Davis, and David Rager.
ACL2 under MacPorts for Mac OS X, courtesy of Greg Wright. Information on MacPorts is available from http://www.macports.org.