Follow these instructions in labs in the basement of ENS (ENS 1 or ENS 2).
cs313k, and click Finish.
cs313k, but if it doesn't, Browse to your new project,
cs313k. Finally, pick a file name, like
defuns.lisp. Select the ACL2 mode Programming (no proofs or soundness requirements/guarantees). Click Finish.
defuns.lisp. You may wish to kill the other panes, by clicking on the X beside the tab name, e.g.,
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.
defuns.lisptab. 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)))))
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.
defuns.lisp.a2stab 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.
fact: Click on ACL2s | Advance Todo. If you typed the definition of
factexactly as shown, then the edit window now has the definition of
factshaded 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
facthas 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
factin the edit window. When you've fixed your typo, try Advance Todo again.
(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
(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)))
defuns.lisp.a2stab says “(not running)”). You need to (re)start the session with ACL2s | (Re)start Session. Then it will look like it did!
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
cs313k/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. Do not send that to me. Find a way to send me
plain text containing just your session transcript, as by copying the relevant
text into a message.