Using ACL2

[Back to main page of Installation Guide.]

Table of Contents


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

We assume that you have followed the installation instructions to install, under some directory dir, a subdirectory acl2-7.0. The sources and perhaps an executable image are located on that subdirectory. However, if you have not saved an image but instead use the directions for Running Without Building an Executable Image, skip to When ACL2 Starts Up below.

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

mycomputer% dir/acl2-7.0/saved_acl2h

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-7.0/saved_acl2h


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


When ACL2 Starts Up

When you invoke ACL2, you should see the host Common Lisp print a header concerning the ACL2 version, license and copyright.

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

ACL2 !>
If however a host leaves you in Common Lisp's read-eval-print loop, then you'll need to evaluate the Common Lisp expression (ACL2::LP) or simply (LP) if the current package is "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
This will cause a moderately long sequence of commands to be processed, each of which is first printed out as though you had typed it. Each will print some text, generally a proof of some conjecture. None should fail.

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-7.0:

make certify-books-short


Certifying ACL2 Books

The community books, which reside in subdirectory books/, have been contributed mainly by users. The general topic of books is discussed thoroughly in the ACL2 books documentation.

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 community books on a Unix-like system. We recommend you do this. If you have entered ACL2, exit to the operating system, e.g., evaluting the form, (quit), or by control-d in many systems.

While connected to dir/acl2-7.0, execute

make certify-books
This will generate minimal output to the screen and will probably take an hour or two. Failure is indicated by the presence of CERTIFICATION FAILED in the log.

To remove the files thus created, invoke:

make clean-books

The certify-books target does not certify the workshops/ books, which include contributions starting with the 1999 ACL2 workshop (described in teh book Computer-Aided Reasoning: ACL2 Case Studies) and include contributions from all subsequent ACL2 workshops. If you want to certify those books as well, then instead (or in addition) use the regression target:

make regression
Our main installation page contains a discussion of options for the above command.

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

make certify-books ACL2=my-acl2

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

We apologize to users of other than Unix-like systems (i.e., other than Unix, GNU-Linux, and Mac OS X): we do not provide instructions for recertifying all the community books on such systems, though there are such environments that can be installed on Windows (e.g., Cygwin). The certification methods provided by the authors of the books vary greatly and we codified them in the makefile, which is named GNUmakefile, used above. Some subdirectories of the community book (under acl2-7.0/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

Documentation is discussed in the section on the User's Manual on the ACL2 home page.

Emacs

Emacs users may find it helpful to load into emacs the file dir/acl2-7.0/emacs/emacs-acl2.el. Utilities offered by this file are documented near the top of the file. In particular, this file automatically loads the ACL2-Doc Emacs browser.

[Back to Installation Guide.]