ACL2 Version 3.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 (md5sum file)

WARNING: Regressions have occasionally stalled with this binary, using "make -j 2 regression". Future OpenMCL releases may solve this problem.

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.1 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 Snaphot 12/5/06 x86-64 (md5sum file)

WARNING: A regression attempt stalled with this binary. Future OpenMCL releases may solve this problem.

Extract this file (creating subdirectory openmcl-1.1-darwinx8664-061205-acl2) with:
```
tar xvfz openmcl-1.1-darwinx8664-061205-acl2.tgz
```
Move the two resulting files into your acl2-sources directory (and then you may delete the empty directory openmcl-1.1-darwinx8664-061205-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/openmcl-1.1pre-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-061205.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.1 sources, used together with this dppccl in the creation of file saved_acl2.dppccl, from the ACL2 home page.

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 darwinports for Mac OS X, courtesy of Greg Wright. Information on darwinports is available from http://darwinports.opendarwin.org.