How to Use ACL2s

``ACL2'' stands for ``A Computational Logic for Applicative Common Lisp.'' It is a theorem proving system developed primarily by Matt Kaufmann and J Strother Moore. See the ACL2 home page for documentation and installation instructions. Most ACL2 experts run ACL2 in a shell buffer under Emacs. If you are familiar with Emacs, you may wish to do that.

The ``ACL2 Sedan'' or ``ACL2s'' is an Eclipse based interface to ACL2 that protects the new user from common mistakes and offers helpful syntax checking, termination analysis, and testing facilities. ACL2s was developed by Peter Dillinger, Pete Manolios and Harsh Chamarthi, of Northeastern University, Boston.

These instructions demonstrate how to use ACL2s. ACL2s is installed on the CS department's public machines. You may carry out this demonstration on one of those machines, or you may first wish to install it on your own machine following the installation instructures here. If you do install ACL2s, you might want to look at the Installation FAQ which addresses several commonly-occurring installation problems.

Start Eclipse: Start | Programs | Programming | Eclipse
Create a project: Select File | New | Project... | General | Project. Then click on Next >;. Enter a new project name that will contain your ACL2 developments for this class, e.g., cs378-jvm, and click Finish.
Open the ACL2 Development perspective: Select Window | Open Perspective | Other | ACL2 Development. Then click OK. This may change the layout of your workbench.
Create a new Lisp file: Select File | New | ACL2s/Lisp file. The “Directory” should already indicate the project you just created, cs378-jvm, but if it doesn't, Browse to your new project, cs378-jvm. Finally, pick a file name, like defuns.lisp. Select the ACL2 mode Programming (no proofs or soundness requirements/guarantees). Click Finish.
Note: You may now have several panes or windows on your screen, each with a tab. One of them will read defuns.lisp. You may wish to kill the other panes, by clicking on the X beside the tab name, e.g., Navigator, Proof Tree, etc. This is just a matter of how you like to manage your screen real-estate.

You should not have to do any of the above again. You could do all your future programming in defuns.lisp if you wish, or you could create different files for different assignments, etc. Good practice is to separate your code into modules (called “books” in ACL2). But that requires you to include the appropriate supporting books when you start developing a new one.
Enter a sample definition: Click on the defuns.lisp tab. We will call this the editor window because it is here you will enter new forms and edit them until you're satisfied they say what you mean. Type this definition in the editor window, to get a feel for the auto-indenting, parenthesis-matching, and syntax-based coloring.
```
(defun fact (n)
  (if (zp n)
    1
    (* n (fact (- n 1)))))
```
Learn a little about the buttons: If you click on ACL2s it will display the icons that also appear on the toolbar and will give you the descriptive name of each icon. We refer to the icons by these names below. But once you learn the icons you won't have to click on ACL2s.
Start a session so you can run your definitions: Click on ACL2s | (Re)start Session. A new tab will appear with a session named defuns.lisp.a2s. Note that you can click on the name of either tab and the contents of that window will be displayed. You will only need these two tabs: defuns.lisp, the editor window and defuns.lisp.a2s, the session window.

Note: If you've never run ACL2s before, the attempt to start a new session will pop up a series of windows asking if you want to certify the ACL2s books. Answer affirmatively to get through this one-time-only certification. It takes a minute or so. Then, hit ACL2s | (Re)start Session again and it should start without error.
Optional - split your Eclipse window so both windows are displayed: You may not have to do this if you've been using Eclipse. But to split the windows, select the defuns.lisp.a2s tab and then click and drag it to the far right-hand edge of the Eclipse frame. A vertical line will appear in the middle of the Eclipse frame. Then unclick. Now both the edit and session windows should appear side-by-side. You may click-and-drag the vertical bar separating them to narrow or widen one of the windows.
Define fact: Click on ACL2s | Advance Todo. If you typed the definition of fact exactly as shown, then the edit window now has the definition of fact shaded gray and the session window will now have this at the bottom:
```
ACL2 p>EVENT
(defun fact (n)
  (if (zp n)
    1
    (* n (fact (- n 1)))))

Summary
Form:  ( DEFUN FACT ...)
Rules: NIL
Warnings:  None
Time:  0.00 seconds (prove: 0.00, print: 0.00, proof tree: 0.00, other: 0.00)
 FACT
ACL2 p>
```
Your colors may vary. If your session window looks like this, then the definition of fact has been accepted. Otherwise, there is an error message in the session window and you should use it to tell you how to fix your definition of fact in the edit window. When you've fixed your typo, try Advance Todo again.
Run a test: In the edit window type (fact 6) below the (defun fact ...). When you're satisfied that you've typed it correctly, Advance Todo again. This should cause the gray area to grow to cover the (fact 6) and it will add
```
ACL2 p>VALUE (fact 6)
720
ACL2 p>
```
to the bottom of the session window. Congratulations! You've just computed factorial of 6! The answer is 720.
Run another test: In the edit window type
```
(cons "Hi" (cons "from" (cons α nil)))
```
where α is your name enclosed in double quotation marks. For example, I would type:
```
(cons "Hi" (cons "from" (cons "J Moore" nil)))
```
Now let's pretend you are finished with this ACL2s session and practice saving the session and quitting.
Whenever you finish with an ACL2s session, quit Eclipse — Click on File | Exit, or (on my Mac) Eclipse | Quit Eclipse. Save all the files it asks about. When you start ACL2s up the next time, it will look ALMOST like it does right now. Try it. Note that the gray area is green and the session isn't running (the defuns.lisp.a2s tab says “(not running)”). You need to (re)start the session with ACL2s | (Re)start Session. Then it will look like it did!
I may sometime ask you to send me an ACL2s session log as a plain text file. The way I do this is to select the Session window, use the standard Edit options, Select All and Copy, to copy the transcript. Then I paste that text into my favorite word processor. If necessary, I'd then use my word processor to delete irrelevant parts of the transcript. Then, using your favorite word processor, add at the top of the file:
- some title “CS378 JVM Question”
- your name
- your EID
- the date
and save the file as a plain text (ASCII) file. If I want the replayable ACL2s script, I'll ask for it.
Warning: If you save the defuns.lisp.a2s window using the Eclipse File | Save options, you will have a file of that name in your Eclipse workspace cs378-jvm/defuns.lisp.a2s. But this file is not easily human readable. It contains a lot of stuff that ACL2s uses to recover the state upon start-up. Find a way to turn in plain text containing just your session transcript.

From here on, I'll assume you can fire up ACL2s, define functions, run expressions, save the transcript, and save your work.