|
|
|---|
|
|
|
|---|
Using ACL2
Table of Contents
We assume that you have followed the installation instructions to install ACL2. The sources and, in general, an executable image are located in that directory. However, if you have not saved an executable image but instead use the directions for running ACL2 without building an executable image (see running-ACL2-without-executable), skip to “When ACL2 Starts Up” below.
Invoke ACL2 by running the executable file,
mycomputer% ./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.,
#!/bin/sh <path>/saved_acl2 "$@"
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 !>
In the very unlikely case that a host leaves you in Common Lisp's
read-eval-print loop, then you'll need to evaluate the Common Lisp expression
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
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 the ACL2 loop. That said, this is typically safe and many users do it. For example, you might exit the ACL2 loop, activate some debugging or trace features in raw Lisp, and then reenter the ACL2 loop. While developing proofs or tracking down problems, this can occasionally be reasonable behavior.
Now you are ready to test your copy of 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 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; see community-books and certify-book. This certification 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
The
Books should be certified before they are used. ACL2 is distributed without book certificates, 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. See installation, or more specifically installation-summary, for how to perform this certification. For additional explanation and further options, see books-certification.
See documentation for a discussion of ACL2's documentation system.
To query ACL2 about a built-in topic,
Emacs users may find it helpful to load into emacs the file