ACL2 Version 2.8 Installation Guide

Creating An Executable Image

• Building an Executable Image on a Unix or Linux System
• Building an Executable Image on Other than Unix and Linux Systems
• Running Without Building an Executable Image

Short Cut: Pre-Built ACL2 Images

Note that the Debian images may work with other Linux systems as well.

Now proceed to Using ACL2.

Building an Executable Image on a Unix or Linux System

By default, if no LISP=xxx is specified, LISP=gcl is used. On our hosts, gcl is the name of GNU Common Lisp, which can be obtained as explained above.

The time taken to carry out this process depends on the host processor but may be only a few minutes for a fast processor. The size of the resulting binary image is dependent on which Lisp was used, but it may be in the vicinity of 17 megabytes.

This make works for the Common Lisps listed in Requirements above on Unix and Linux systems we have tested. See the file acl2-sources/Makefile for further details. If this make command does not work for you, please see the instructions for non-Unix/Linux systems below.

You can now skip to Using ACL2.

Building an Executable Image on Other than Unix and Linux Systems

If you are building under Windows using GCL, you may want to proceed directly to instructions for building on Windows using GCL.

Otherwise, proceed as follows.

Your Common Lisp should be one of those listed in Requirements above. Filenames below should default to the dir/acl2-sources directory, e.g., for GCL, connect to dir/acl2-sources before invoking GCL or, after entering GCL, do (si::chdir "dir/acl2-sources/").

1. Remove file nsaved_acl2 if it exists.

2. Start up Common Lisp in the acl2-sources directory and submit the following sequence of commands.

     ; Compile
     (load "init.lsp")
     (in-package "ACL2")
     (compile-acl2)
   

   The commands above will compile the ACL2 sources and create compiled object files on your acl2-sources subdirectory.

3. Now exit your Common Lisp and invoke a fresh copy of it (mainly to avoid saving an image with the garbage created by the compilation process). Again arrange to connect to the acl2-sources subdirectory. In the fresh Lisp type:

     ; Initialization, first pass
     (load "init.lsp")
     (in-package "ACL2")
     (load-acl2)
     (initialize-acl2 (quote include-book) *acl2-pass-2-files* t t)
   

   This will load the new object files in the Lisp image and bootstrap ACL2 by reading and processing the source files. But the attempt at initialization will end in an error saying that it is impossible to finish because a certain file was compiled during the processing, thus dirtying the image yet again. (If however the attempt ends with an error during compilation of file TMP1.lisp, see the first troubleshooting tip below.)

4. So now exit your Common Lisp and invoke a fresh copy of it (again arranging to connect to your acl2-sources subdirectory). Then, in the fresh Lisp type:

     ; Initialization, second pass
     (load "init.lsp")
     (in-package "ACL2")
     (save-acl2 (quote (initialize-acl2 (quote include-book) *acl2-pass-2-files* t))
                "saved_acl2")
   

   You have now saved an image. Exit Lisp now. Subsequent steps will put the image in the right place.

5. Remove osaved_acl2 if it exists.

6. IF saved_acl2 and saved_acl2.dxl both exist THEN:
   • move saved_acl2.dxl to osaved_acl2.dxl
   • move saved_acl2 to osaved_acl2 and edit osaved_acl2, changing saved_acl2.dxl (at end of line) to osaved_acl2.dxl
   ELSE IF saved_acl2 exists THEN:
   • move saved_acl2 to osaved_acl2

7. Move nsaved_acl2 to saved_acl2.

8. For Allegro Common Lisp, Versions 5.0 and later, nsaved_acl2.dxl should exist; move it to saved_acl2.dxl

9. Make sure saved_acl2 is executable.

Special Case: Building an Executable Image on a Windows System using GCL

1. FIRST get GCL running on your Windows system using ONE of the following two options. Note that GCL can be unhappy with spaces in filenames, so you should probably save the GCL distribution to a directory whose path is free of spaces.
   • OR, obtain GCL for Windows systems from ftp://ftp.gnu.org/gnu/gcl/ or as explained above. You may wish to pick a .zip file from the cvs/ subdirectory (containing pre-releases) that has "mingw32" in the name.
   • OR ELSE, perhaps you can build GCL on your Windows system from the sources. The mingw tools and the cygnus bash shell have been used to build distributed GCL executables.
2. SECOND, create an appropriate GCL batch file. When we tried running the script gclm/bin/gclm.bat that came with gcl-cvs-20021014-mingw32 from the above ftp site, a separate window popped up, and with an error. Many ACL2 users prefer running in an emacs shell buffer. (We obtained emacs for Windows from ftp://ftp.gnu.org/gnu/windows/emacs/21.2/emacs-21.2-fullbin-i386.tar.gz.) The following modification of gclm.bat seemed to solve the problem (your pathnames may vary).

   @
   % do not delete this line %
   @ECHO off
   set cwd=%cd%
   path C:\gcl\gclm\mingw\bin;%PATH%
   C:\gcl\gclm\lib\gcl-2.6.1\unixport\saved_gcl.exe -dir C:/gcl/gclm/lib/gcl-2.6.1/unixport/ -libdir  C:/gcl/gclm/lib/gcl-2.6.1/ -eval "(setq si::*allow-gzipped-file* t)" %1 %2 %3 %4 %5 %6 %7 %8 %9
   

3. THIRD, follow the instructions for non-Unix/Linux systems above, though the resulting file may be called saved_acl2.exe rather than saved_acl2.
4. FINALLY, create a file acl2.bat as explained in ftp://ftp.cs.utexas.edu/pub/moore/acl2/v2-8/images/README.html.

We hope that the above simply works. If you experience problems, the following hints may help.

TROUBLESHOOTING:

• We tried building ACL2 on Windows XP on top of GCL, our attempt broke at the end of the "Initialization, first pass" step, while compiling TMP1.lisp. That was easily remedied by starting up a fresh GCL session and invoking (compile-file "TMP1.lisp") before proceeding to the next step.
• Yishai Feldman has provided some nice instructions at http://www.faculty.idc.ac.il/yishai/reasoning/win-install.htm, some of which we have tried to incorporate here. A useful point made there is that when you want to quit ACL2, use :good-bye (or (good-bye) which works even in raw Lisp). Or you can use (user::bye) in raw Lisp. The point is: Avoid control-c control-d, even thought that often works fine in emacs under Unix/Linux.
• If the above batch file does not work for some reason, an alternate approach may be to set environment variables. You may be able to add to the PATH variable gcl-dir\gcc\bin, where gcl-dir is the directory where GCL is installed. To get to the place to set environment variables, you might be able to go to the control panel, under system, under advanced. Alternately, you might be able to get there by opening My Computer and right-clicking to get to Properties, then selecting the Advanced tab. At one time, when GCL/Windows was release as Maxima, Pete Manolios suggested adding the system variable LD_LIBRARY_PATH with the value "maxima-dir\gcc\i386-mingw32msvc\include"; this may or may not be necessary for your GCL installation (and the path would of course likely be different).

Running Without Building an Executable Image

We assume you have obtained ACL2 and placed it in directory dir, as described above for Unix/Linux or other platforms. If you downloaded a pre-built ACL2 image, then you may skip this section. Otherwise, connect to subdirectory acl2-sources of dir, start up your Common Lisp, and compile by executing the following forms. This sequence of steps need only be performed once.

  (load "init.lsp")
  (in-package "ACL2")
  (compile-acl2 nil)

  (load "init.lsp")
  (in-package "ACL2")
  (load-acl2 nil)
  (initialize-acl2 (quote include-book) *acl2-pass-2-files* nil)

Now proceed to read more about Using ACL2.

Summary of Distribution

README.html; This file
acl2-sources/
  LICENSE  ; GNU General Public License
  Makefile ; For Unix/Linux make.  See README.
  TAGS     ; Handy for looking at source files with emacs
  *.lisp   ; ACL2 source files
  all-files.txt   ; List of all files in this directory and subdirectories
  books/   ; Examples, potentially useful in others' proofs.  See books/README.html.
  doc/     ; ACL2 documentation in various formats
  emacs/   ; Miscellaneous emacs and file utilities, especially emacs-acl2.el
  init.lsp ; Useful for building the system
  interface/
    emacs/ ; Support for ACL2 "proof trees".  See interface/emacs/README.doc.
    infix/ ; ACL2 infix printer by Mike Smith.  See interface/infix/README.
  saved/   ; Empty directory for backing up copies during make; not important
acl2.tar.gz; gzip'd tar file containing all of acl2-sources/ (see below)
images/    ; Some gzip'd tar'd executables; see images/README
split/     ; The result of splitting up acl2.tar.gz; see split/README

The entire acl2.tar.gz is roughly 4.6 megabytes, which expands out to roughly 19 megabytes. Additional space is required to build an image, perhaps 17 megabytes (though this depends on the Lisp), and to certify books.

Saving Space

USING ACL2

Invoking ACL2

The executable image is called acl2-sources/saved_acl2. You can invoke ACL2 by running that image, e.g.,

mycomputer% dir/acl2-sources/saved_acl2

If on a Unix/Linux system, then to make it easy to invoke ACL2 by typing a short command, e.g.,

mycomputer% acl2

you may want to install an executable file on your path, e.g., /usr/local/bin/acl2, containing the following two lines:

#!/bin/csh -f
dir/acl2-sources/saved_acl2


Note: A carriage return in the file after the last line above is important!

Instructions from Jared Davis for building ACL2 on Windows using mingw

	      Building ACL2 on Windows from Scratch
   _____________________________________________________________

   Note: The disk space requirements are large.  Not including
   emacs, I had about 275 MB taken up by msys/mingw32/gcl/acl2
   during the build process.  You can probably use much less
   space by removing files after you use them, but I didn't
   bother to do that.

   Here are the steps I took:

   Downloaded emacs 21.3 full distribution and installed
   Downloaded msys 1.10.10, installed to c:\acl2
   Downloaded mingw 3.1.0-1, installed to c:\acl2\mingw
   Downloaded gcl 2.5.3, extracted to c:\acl2\mingw
   Downloaded acl2 2.8, extracted to c:\acl2\sources



   Compiling gcl:

     in msys:

       cd /acl2/ming2/gcl-2.5.3
       ./configure
       make
       make install



   Compiling acl2:

     copy "etags.exe" to /mingw/bin.  you can find this program
     in your emacs folder, under "bin".

     in msys:

       cd /sources
       make



   Certifying ACL2 books:
   This took 111 minutes on my Athlon 2500+

     in msys:

       cd /sources

       mv nsaved_acl2.gcl.exe saved_acl2.exe

       vim books/Makefile-generic, remove "nice" from this line:
	   ACL2=time nice ../../saved_acl2

       make certify-books ACL2=/sources/saved_acl2.exe

When ACL2 Starts Up

Some hosts then automatically enter the ACL2 ``command loop,'' an ACL2 read-eval-print loop with the prompt:

ACL2 !>

Once in the ACL2 command loop, you can type an ACL2 term, typically followed by ``return'' or ``enter,'' and ACL2 will evaluate the term, print its value, and prompt you for another one. Below are three simple interactions:

ACL2 !>t
T
ACL2 !>'abc
ABC
ACL2 !>(+ 2 2)
4

To get out of the ACL2 command loop, type the :q command. This returns you to the host Common Lisp. We sometimes call this ``raw Lisp.'' You may re-enter the command loop with (LP) as above.

Note that when you are in raw Lisp you can overwrite or destroy ACL2 by executing inappropriate Common Lisp expressions. All bets are off once you've exited our loop. That said, many users do it. For example, you might exit our loop, activate some debugging or trace features in raw Lisp, and then reenter our loop. While developing proofs or tracking down problems, this is reasonable behavior.

Now you are ready to test your image.

Testing ACL2

An easy way to test the theorem prover is to type the following term to the ACL2 command loop:

:mini-proveall

A more elaborate test is to certify the ``books'' that come with the distribution, which is a good idea anyhow; this is our next topic. On a Unix/Linux system, you can also certify just a small but useful subset of the books in a few minutes by executing, in the top-level ACL2 directory (called dir: above):

make certify-books-short

Certifying ACL2 Books

Books should be ``certified'' before they are used. We do not distribute certificates with our books, mainly because certification produces compiled code specific to the host. You should certify the books locally as a test of your ACL2 image.

It is easy to re-certify all the distributed books in Unix/Linux. We recommend you do this. If you have entered ACL2, exit to the operating system, e.g., by control-d in many systems.

While connected to dir/acl2-sources, execute

make certify-books

make clean-books

The certify-books target does not cause workshop books to be certified. If you want to certify those books as well, you will first need to download the gzipped tar file to the books/ directory, and then gunzip and extract it. You can certify all the books, including books for the workshops (including those from the 1999 workshop as described in the (hardbound) book Computer-Aided Reasoning: ACL2 Case Studies), using the command:

make regression

By default, certification uses the image dir/acl2-sources/saved_acl2. You may specify any ACL2 image, as long as it is either a command on your Unix/Linux path or an absolute file name, for example as follows.

make certify-books ACL2=my-acl2

make regression ACL2=/u/smith/projects/acl2/saved_acl2

We apologize to non-Unix/Linux users: we do not provide non-Unix/Linux instructions for recertifying the distributed books. The certification methods provided by the authors of the books vary greatly and we codified them in the Unix/Linux Makefile used above. Most subdirectories of acl2-sources/books contain either a README file or a certify.lsp file. Users who wish to certify one of these books and who cannot figure out (from these scant clues) what to type to ACL2 should not hesitate to contact the authors.

Next proceed to the section on Documentation.

Documentation

ACL2's documentation is a hypertext document that, if printed in book form, is about 800 pages or about 1.5 megabytes of text. Its hypertext character makes it far more pleasing to read with an interactive browser. The documentation is available in four formats: HTML, Texinfo, Postscript and ACL2 documentation strings. All of this material is copyrighted by the University of Texas at Austin and is derived under the GNU General Public License from material copyrighted by Computational Logic, Inc.

Two Web-based guided tours of ACL2 are available from the home page noted below. If you are already familiar with Nqthm, you might find it useful to look at the documentation node NQTHM-TO-ACL2. Another useful documentation topic for beginning ACL2 users is the node TUTORIAL.

HTML

The ACL2 Home Page is

http://www.cs.utexas.edu/users/moore/acl2/index.html

The home page provides a selected bibliography, a search button (near the top of the page), guided tours of the system, and the complete hypertext documentation tree.

Once you have installed ACL2, the HTML form of the documentation is available locally as dir/acl2-sources/doc/HTML/acl2-doc.html.

We urge you to browse your local copy of the documentation rather than our Web copy, simply to reduce Web traffic and the demand on our server. (Macintosh users using MacOS 9 and earlier may, however, find filenames being truncated and hence will want to avoid the local documentation.)

Emacs Info

This is a very convenient format for accessing the ACL2 documentation from within Emacs. In Emacs, invoke

meta-x info

control-h m