ACL2 Version 3.2.1 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 you can get the ACL2 Version 3.2.1 sources, used together with this dppccl in the creation of file saved_acl2.dppccl, by following links 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.1 sources, used together with this dppccl in the creation of file saved_acl2.dx86cl64, from the ACL2 home page.

Complete Packages:

acl2.tar.gz

Debian packages. Thanks to Camm Maguire for creating and maintaining the Debian packages for ACL2.
Windows Installers. Thanks to Alex Spiridonov and Jared Davis. (As of this writing none has been created for ACL2 Version 3.2.1. Feel free to volunteer to create one! Just send email to Matt Kaufmann if you care to volunteer.
ACL2 under MacPorts for Mac OS X, courtesy of Greg Wright. Information on MacPorts is available from http://www.macports.org.