Using ACL2

Table of Contents

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

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

Invoking ACL2

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

mycomputer% dir/acl2-8.3/saved_acl2

If you on a Unix-like 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-8.3/saved_acl2


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

When ACL2 Starts Up

Most or all 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 community books, which is a good idea anyhow; this is our next topic. On a Unix-like system, you can also certify just a small but useful subset of the books in a few minutes by executing, in directory dir/acl2-8.3:

make basic

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. Our main installation page contains simple instructions for how to perform this certification. For additional explanation and further options, see the documentation for BOOKS-CERTIFICATION.

Next proceed to the section on Documentation.

Documentation

Emacs