Using ACL2

Table of Contents

• Invoking ACL2
  • When ACL2 Starts Up
• Testing ACL2
• Certifying ACL2 Books
• Documentation

Here we begin with a discussion of how to invoke ACL2 interactively. We then discuss testing as well as the certification of ACL2 books that come with the distribution. We conclude with a discussion of the documentation.

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!

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 directory dir/acl2-sources:

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, both as a test of your ACL2 image and because books generally need to be certified before they can be used.

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

To remove the files thus created, invoke:

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 (GNUmakefile) 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 1100 pages or more than 2 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

Users new to emacs may find it helpful to load into emacs the file dir/acl2-sources/emacs/emacs-acl2.el. Utilities offered by this file are documented near the top of the file.

Postscript

The Postscript version of the documentation is not included in our normal distribution because it is so much less useful than the hyper-text versions. But a gzipped Postscript (1.2 MB) version is available. It prints as a book of about 1000 pages and contains a Table of Contents and an index to all documented topics.

ACL2 Documentation Strings

The ACL2 system has facilities for browsing the documentation. When you are in the ACL2 command loop, you may query the documentation on a given topic by typing the command

:doc topic

where topic is the Lisp symbol naming the topic you want to learn about. To learn more about the on-line documentation, type :help and then return.

Note, however, that you may find it more convenient to view the documentation in a web browser (starting at doc/HTML/acl2-doc.html) or in Emacs info (starting at doc/EMACS/acl2-doc-emacs.info).

[Back to Installation Guide.]