ACL2 Version 3.3 Images

Executable Images

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.

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 ACL2 for OpenMCL
  See the instructions below for installing one of the following gzipped tar files.
  • Gzipped ACL2 for OpenMCL on Darwin/PowerPC (md5sum file)
  • Gzipped ACL2 for OpenMCL on Darwin/x86 (64-bit only) (md5sum file)
  • Gzipped ACL2 for OpenMCL on Linux (64-bit only) (md5sum file)
  Extract this file, to create a subdirectory named openmcl-darwinppc-snapshot-r7591-acl2/ in the first case, or analogously replacing "darwinx8664" or "linuxx8664" if you retrieve the second or third file above.

  tar xvfz openmcl-darwinppc-snapshot-r7591-acl2.tgz
  

  Move the two resulting files into your acl2-sources/ directory (and then you may delete the empty subdirectory). Create a wrapper script, say, saved_acl2 or 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, and replace EXTENSION with either dppccl, dx86cl64, or lx86cl64 depending on whether you fetched the first, second, or third file above, respectively.

  ---

  #!/bin/sh
  export ACL2_SYSTEM_BOOKS=ACL2_DIR/books
  "OPENMCL_DIR/EXTENSION" -I "ACL2_DIR/saved_acl2.EXTENSION" -e "(acl2::acl2-default-restart)" $*
  

  ---

  You'll need to save the above wrapper script as an executable file (chmod +x openmcl-saved_acl2).
  Note: You can get the Open MCL sources from which this binary was created, from the following three URLs, listed in the same order as the files above.
  • ftp://clozure.com/pub/openmcl-snapshots-for-ACL2/openmcl-darwinppc-snapshot-r7591.tar.gz
  • ftp://clozure.com/pub/openmcl-snapshots-for-ACL2/openmcl-darwinx8664-snapshot-r7591.tar.gz
  • ftp://clozure.com/pub/openmcl-snapshots-for-ACL2/openmcl-linuxx8664-snapshot-r7591.tar.gz
  And of course, you can get the ACL2 Version 3.3 sources, used together with this OpenMCL binary in creation of executable saved_acl2.EXTENSION, 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, but it may work fine on 64-bit Intel-based Macs.

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.3 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:

• 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.