Determine from local experts whether acl2 is installed on your system. If
not, you can install it from
ACL2. Try invoking ACL2 with
acl2.
ACL2 provides a ``read-eval-print'' command loop
ACL2 !>:program ; enter program mode ACL2 p>:redef ; allow redefinitions ACL2 p!>(your input form here)<Return> ; this is a comment (value printed here) ACL2 p!> ; waiting for your next input
To exit ACL2 to ``raw Common Lisp'' type :q.
To enter ACL2 from raw Common Lisp, type (LP).
Use a text editor! Most ACL2 users choose Emacs. Prepare
Lisp definitions in an edit buffer and save them to .lisp
``script'' files. Definitions must be presented in a ``bottom-up''
style: primitive subroutines first; top-level functions last.
Submit commands one at a time in
:program mode to check syntax. Type test expressions directly
to ACL2 or put them in your script, possibly as #|comments|#.
To load a script use (ld "script.lisp") or
use include-book if your script is a book.
X, x, alist, temp2, prev-temp
23, -7, 22/7, #c(3 5)
#\A, #\a, #\, , #\Newline, #\Space
"Test", "He said \"Hi!\" as we passed."
t, nil, 'ABC, 'abc, 'true-list, :key, math::abs, |John|'(1 2 3), '((A . 1) (B . 2)), '((1 . 2) . (3 . 4))
(fn arg1 arg2 ... argn)(in-package "pkg")
(defpkg "pkg" '(imported symbols))
(program) or
:program
|
for prototyping a system of definitions and testing it on examples |
(logic) or
:logic
|
for defining functions, proving termination and other properties |
(redef) or
:redef
|
allow redefinitions of functions |
(defconst *var* term)
(defun fn (var1 ... varn) (declare (xargs :measure term1 ; declarations are optional :guard term2 :hints hints ...others)) body)or
(mutual-recursion (defun ...) ... (defun ...))
:set-guard-checking t/nil
:comp t
:u
|
undo last command and prints most recent surviving command |
:ubt cmd
|
undo back through the command described by cmd |
:ubt! cmd
|
undo back through with no questions asked |
:pbt cmd
|
print back through |
:pc cmd
|
print command named cmd (:x is most recent command)
|
:pe name
|
print event, e.g., function definition or theorem, named name |
Control | |
(if x y z)
|
if x is non-nil then y else z |
(equal x y)
|
equality predicate |
(cond (x1 y1) (x2 y2) ... (t z)) |
(if x1 y1
(if x2 y2
...
z))
|
(case key (c1 y1) (c2 y2) ... (t z)) |
(cond ((equal key 'c1) y1) ((equal key 'c2) y2) ... (t z)) |
(let ((var1 val1) ...) body)
|
bind local variables in parallel |
(let* ((var1 val1) ...) body)
|
bind local variables sequentially |
(mv-let (var1 ...) vector body)
|
bind local variables to vector of multiple values |
(mv val1 ...)
|
return a vector of multiple values |
Boolean | |
(and p q ...)
|
lazy logical conjunction operator |
(or p q ...)
|
lazy logical disjunction operator |
(implies p q)
|
logical implication |
(not p)
|
logical negation |
(iff p q)
|
logical equivalence |
Arithmetic | |
(acl2-numberp x)
|
recognizer for any type of ACL2 number |
(integerp x)
|
recognizer for integers |
(rationalp x)
|
recognizer for rationals |
(complex-rationalp x)
|
recognizer for complex numbers |
(equal x 0),
(zerop x),
(zip x),
(zp x)
|
several ``idioms'' for ``x=0'' |
(< x y)
|
less than relation |
(<= x y)
|
less than or equal relation |
(> x y)
|
greater than relation |
(>= x y)
|
greater than or equal relation |
(+ x y ...)
|
addition operator |
(* x y ...)
|
multiplication operator |
(- x y)
|
subtration operator |
(- x)
|
arithmetic negation |
(/ x y)
|
rational division |
(1- x)
|
decrement by 1 |
(1+ x)
|
increment by 1 |
(numerator r)
|
numerator of a rational number |
(denominator r)
|
denominator of a rational number |
(realpart c)
|
``real'' part of a complex |
(imagpart c)
|
``imaginary'' part of a complex |
(complex r i)
|
make complex number with rational components |
Characters | |
(characterp x)
|
recognizer for character objects |
(char-code char)
|
convert character to integer code |
(code-char n)
|
convert integer code to character |
Strings | |
(stringp x)
|
recognizer for string objects |
(char str n)
|
fetch the nth character of a string |
(coerce str 'LIST)
|
convert a string to a list of characters |
(coerce charlist 'STRING)
|
convert a list of characters to a string |
(length str)
|
length of a string (or of a list) |
Symbols | |
(symbolp x)
|
recognizer for symbols |
(symbol-name sym)
|
string giving the print name of a symbol |
(symbol-package-name sym)
|
string naming the package a symbol is in |
(intern-in-package-of-symbol str pkg)
|
construct a symbol with a given name and package |
Cons Pairs and Lists | |
(consp x)
|
recognizer for ordered pairs |
(cons x y)
|
construct an ordered pair |
(car pair)
|
first component of an ordered pair |
(cdr pair)
|
second component of an ordered pair |
(endp x)
|
recognizer for non-pairs |
(atom x)
|
recognizer for non-pairs |
(list x0 x1 ... xk)
|
true list of given objects |
(list* x0 x1 ... xk cdrk)
|
list of objects with cdrk as ``last'' cdr |
(caar pair)
|
car of the car |
(cadr pair)
|
car of the cdr |
(cdar pair)
|
cdr of the car |
(cddr pair)
|
cdr of the cdr |
| ... | ... |
(cddddr pair)
|
cdr of the cdr of the cdr of the cdr |
(append x y ...)
|
concatenate linear lists |
(assoc-equal x alist)
|
lookup in an alist, comparing keys with equal |
(nth n lst)
|
nth element of a linear list (0-based) |
(length list)
|
length of a list (or of a string) |
(true-listp x)
|
recognizer for linear lists |
| General shell stuff | |
| "control-t e" | sends the current form to the shell buffer |
| "control-t b" | switches to the shell buffer |
| "control-t c" | sets the shell buffer (initially, *shell*) to the current buffer |
| "control-t control-e" | sends the current form to the shell buffer, but in the other window |
| "control-d" | redefined in shell/telnet buffers to avoid ending process |
| "meta-p" and "meta-n" | cycle backward/forward doing command completion in shell/telnet buffers |
| "control-<RETURN>" | sets shell/telnet directory buffer to current directory |
|
From current buffer to shell buffer | |
| "control-t l" | prints appropiate ACL2 LD form to the end of the shell buffer, to cause evaluation of the active region in the current buffer |
| "control-t control-l" | prints just as above, but inhibits output and proofs; can easily be edited to inhibit only one or the other |
| "control-t u" | puts an appropriate :ubt at the end of the shell buffer, based on the event in which you are currently standing |
|
Some editing commands | |
| "meta-x find-unbalanced-parentheses" | locates unbalanced parentheses |
| "control-t a" | puts line with cursor at bottom of window |
| "control-t <TAB>" | completes filename in any buffer |
| "control-t control-v" | scrolls half as far as "control-v" |
| "control-t v" | scrolls half as far as "meta-v" |
| "control-t s" | searches forward non-interactively, with string supplied in minibuffer, case-sensitive |
| "control-t control-s" | like "control-t s" above, but case-insensitive (at least by default) |
| "control-meta-q" | indents s-expression even when not in lisp-mode |
| "control-t control-p" | executes "meta-x up-list", moving to end of enclosing s-expression |
| "control-t w" | does "meta-x compare-windows" (see emacs documentation, "control-h f compare-windows", for more info) |
| "control-t q" | is like "control-t w" above, but ignores whitespace (and case too, with a positive prefix argument) |
| "meta-x visit-acl2-tags-table" | sets the current tag table to the one in the ACL2 source directory |
| "control-t f" | fills format strings; see documentation for more info ("control-h f fill-format-string") |
| "control-t control-f" | buries the current buffer (puts it on the bottom of the buffer stack, out of the way, without killing the buffer) |
|
Proof-tree support | |
| "meta-x start-proof-tree" | starts proof-tree tracking in the current buffer (where ACL2 is running). See ACL2 documentation for PROOF-TREE for more information. |
|
Run ACL2 as an inferior process | |
| "meta-x run-acl2" | starts up acl2 as an inferior process in emacs. However, most ACL2 users prefer simply to run ACL2 in an ordinary shell, for example, in Emacs: meta-x shell. |
|
ACL2 proof-checker support | |
| "control-t d" | prints an appropriate DV command at the end of the current buffer, suitable for diving to subexpression after printing with proof-checker "th" or "p" command and then positioning cursor on that subexpression. See ACL2 documentation for PROOF-CHECKER. |
| "control-t control-d" | is like "control-t d" above, but for DIVE command instead (used with "pp" instead of "p") |
|
Miscellaneous | |
| "meta-x acl2-info" | brings up ACL2 documentation in pleasant emacs-info format |
| "meta-x date" | prints the current date and time (commented out) |
| "control-meta-l" |
swaps top buffer with next-to-top buffer (same as "control-x b |
| "control-t" | is a prefix for other commands |
| "control-t control-t" | transposes characters (formerly "control-t") |
| Other features: |
Turn on time/mail display on mode line. Disable a few commands. Calls of case, case!, case-match, mv-let, and dolist will indent like calls of defun. |
Some other features you may want but will need to uncomment in your emacs-acl2.el file; see acl2-sources/emacs/emacs-acl2.el for details: