ACL2 Version 3.2 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>

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.

Gzipped Debian Gnu Linux GCL 2.6.7 image (md5sum file)

Here is the wrapper script. Replace ACL2_DIR by your acl2-sources/ directory path.
```
#!/bin/sh
export ACL2_SYSTEM_BOOKS=ACL2_DIR/books
exec "ACL2_DIR/debian-gnu-linux-gcl-saved_acl2.gcl" $*
```

Gzipped ACL2 for OpenMCL 1.0 Darwin/PowerPC (Macintosh) (md5sum file)

Extract this file (creating subdirectory openmcl-1.0-ppc-acl2/) with:
```
tar xvfz openmcl-1.0-ppc-acl2.tgz
```
Move the two resulting files into your acl2-sources directory (and then you may delete the empty directory openmcl-1.0-ppc-acl2/). Create a wrapper script, say, openmcl-saved_acl2, to reside in the same directory as the two extracted files and as your acl2-sources directory. Simply modify the script below: replace both ACL2_DIR and OPENMCL_DIR by your acl2-sources/ directory path.
```
#!/bin/sh
export ACL2_SYSTEM_BOOKS=ACL2_DIR/books
"OPENMCL_DIR/dppccl" -I "ACL2_DIR/saved_acl2.dppccl" -e "(acl2::acl2-default-restart)" $*
```
You'll need to save it as an executable file (chmod +x openmcl-saved_acl2).
Note: You can get the Open MCL 1.0 sources, from which this distributed binary dppccl was created, from: http://openmcl.clozure.com/. And of course, you can get the ACL2 Version 3.2 sources, used together with this dppccl in the creation of file saved_acl2.dppccl, from the ACL2 home page.

Gzipped ACL2 for OpenMCL 1.1 Darwin (Macintosh) Snapshot 5/12/07 x86-64 (md5sum file)

Extract this file (creating subdirectory openmcl-1.1-darwinx8664-070512-acl2) with:
```
tar xvfz openmcl-1.1-darwinx8664-070512-acl2.tgz
```
Move the two resulting files into your acl2-sources directory (and then you may delete the empty directory openmcl-1.1-darwinx8664-070512-acl2). Create a wrapper script, say, openmcl-saved_acl2, to reside in the same directory as the two extracted files and as your acl2-sources directory. Simply modify the script below: replace both ACL2_DIR and OPENMCL_DIR by your acl2-sources/ directory path.
```
#!/bin/sh
export ACL2_SYSTEM_BOOKS=ACL2_DIR/books
"OPENMCL_DIR/dx86cl64" -I "ACL2_DIR/saved_acl2.dx86cl64" -e "(acl2::acl2-default-restart)" $*
```
You'll need to save it as an executable file (chmod +x openmcl-saved_acl2).
Note: You can get the Open MCL sources from which this distributed binary dppccl was created, from file openmcl-darwinx8664-snapshot-070512.tar.gz at: ftp://clozure.com/pub/testing/ As of this writing, the above file is there; later, you can find it in the archive/ subdirectory. And of course, you can get the ACL2 Version 3.2 sources, used together with this dppccl in the creation of file saved_acl2.dx86cl64, from the ACL2 home page.

Gzipped ACL2 for SBCL 1.0 on Intel-based Macintosh machines (md5sum file)

Note: We have tested this on a 32-bit Intel-based Macintosh. We have tested it only minimally on a 64-bit Intel-based Macintosh.
Extract this file (creating subdirectory sbcl-1.0-x86-acl2) with:
```
tar xvfz sbcl-1.0-x86-acl2.tgz
```
Move the two resulting files into your acl2-sources directory (and then you may delete the empty directory sbcl-1.0-x86-acl2). Create a wrapper script, say, sbcl-saved_acl2, to reside in the same directory as the two extracted files and as your acl2-sources directory. Simply modify the script below: replace ACL2_DIR by your acl2-sources/ directory path.
```
#!/bin/sh
export ACL2_SYSTEM_BOOKS=ACL2_DIR/books
exec "ACL2_DIR/sbcl" --core "ACL2_DIR/sbcl-saved_acl2.core" --userinit /dev/null --eval '(acl2::sbcl-restart)'
```
You'll need to save each file as an executable file:
```
chmod +x sbcl-saved_acl2
chmod +x sbcl
```
Note: You can get the SBCL 1.0 sources from which this distributed binary dppccl was created, from file http://heanet.dl.sourceforge.net/sourceforge/sbcl/sbcl-1.0-source.tar.bz2; see below for copyright/license info. And of course, you can get the ACL2 Version 3.2 sources, used together with this sbcl binary in the creation of file sbcl-saved_acl2.core, from the ACL2 home page.
License/Copyright info for SBCL 1.0.
File "COPYING" from the SBCL 1.0 distribution says:
Thus, there are no known obstacles to copying, using, and modifying SBCL freely, as long as copyright notices of MIT, Symbolics, Xerox and Gerd Moellmann are retained.
All relevant copyright notices may be found in the SBCL 1.0 sources. We include what we believe is a representative sample here.

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.

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