• Introduction
• Building executables
• DoubleCheck Reference
• Troubleshooting
• Tutorial (reverse)

Windows Mac OS X Linux

Introduction to Proof Pad

The REPL

The REPL, or "Read-Eval-Print loop", is located in the bottom half of the main Proof Pad window. Essentially, the REPL will execute any code you type in the text field on bottom (the "prompt") and show the result in the log above.

Try typing some math into the REPL now:

(+ 1 2)

If ACL2 is functioning correctly, you should get

3

back. (If you don't, see the troubleshooting page.)

There are a couple of things to note at this point. First, the '3' has a checkmark with a green background next to it. This means that the function call executed without errors. A red 'x' means that there was an error, and a '<' sign means that the message is informational (not in direct response to something you did).

The REPL is a good place to test the functions you write in the definitions area, or just to get a sense of how to use a certain function or feature.

The definitions area

The definitions area is where you write your functions, theorems, and other state-altering expressions. Here's a definition for 'sum' that you can either retype or copy and paste:

(defun sum (xs)
(if (endp xs)
0
(+ (first xs)
  (sum (rest xs)))))

When you type or paste this into the definitions area, you might notice that the background color of the proof bar goes from white to grey to light green, and a checkmark appears. This simply means that the code was executed by ACL2 without any problems. We'll talk more about the proof bar in the next section

Definitions occur in an ordered way in the file; if you want to use the function "foo" within the function "bar", you must put the definition of "foo" above the definition of "bar". This has to do with how ACL2 processes events; the ACL2 "world" must be logically consistent after each and every event, so if you used "foo" before defining it, ACL2 might be accepting something that won't actually work.

Proof bar

The proof bar is the (normally white) bar to the left of the definitions panel that allows you to view and manipulate the status of ACL2 with respect to your code.

By default, Proof Pad is passing all of your functions, theorems, tests, etc to ACL2 automatically. This automatic admission occurs in :program mode¹, an ACL2 mode where ACL2 doesn't worry as much about logic. The intent of this is to let you test your functions in the REPL, even if they aren't carefully written enough in the way ACL2 expects to be used in :logic mode.

If the automatic admission succeeds, the proof bar turns light green next to the admitted code. If it fails, it instead turns red, an 'x' is shown, and the details pane opens up to show you the error message you received.

You will probably want to admit these functions to ACL2's :logic mode (a requirement if you want to prove theorems). To do this, click on the proof bar next to the function you want to admit. As you hover over the proof bar, it will show you a preview of what's going to be done; in particular, if you want to admit an expression, you have to first admit all the expressions above it. The proof bar handles this for you.

Once you've admitted some code to the ACL2 logic (which can take some time for complex functions or theorems), the proof bar turns green next to the form or forms that were admitted. If ACL2 encounters an error, a red 'x' is shown and the error pane opens to show you the response that Proof Pad got from ACL2. If the proof or admission was successful, the error pane won't open up by default. If you're curious about what the ACL2 output was, you can click the '>' sign to the right of the form you admitted (though you rarely care about that if the proof succeeds).

Try admitting your sum function from before.

Admitted code becomes read-only in Proof Pad, since editing it requires re-admitting it to ACL2. To un-admit some code (and thus make it editable), just click on the proof bar again next to the expression you want to edit. Proof Pad will roll back ACL2 to the function you want to edit. You can make your edits and then re-admit.