Advanced-features
Some advanced features of ACL2
Maybe you've been using ACL2 for awhile, and you wonder if there
are lesser-known features that you might find useful. Then this topic is for
you. We present below a ``laundry list'' of some such features, with brief
descriptions and links to documentation topics.
Although the list below is long, it is not intended to be complete, and
indeed some topics have been deliberately excluded. Some have fallen out of
use, perhaps for good reason, such as obdd. Others are already likely
to be discovered when needed, such as getenv$ and perhaps double-rewrite. Some topics are referenced by documentation for others in
the list, such as mbt, which is referenced by mbe. Some
utilities such as pstack and verbose-pstack seem too low-level
to be worthy of inclusion below.
For an extensive introduction to using the prover, which may include some
aspects new to you, see introduction-to-the-theorem-prover. A shorter
topic contains highlights for efficient prover usage: see tips. Also
see ACL2-sedan for an extension of ACL2 (written by others), ACL2s,
that includes an Eclipse-based interface, more powerful and automatic
termination reasoning, and other features.
We now move on to the list.
Top-level commands and utilities:
- See a! and see p! to abort or pop.
- See ACL2-customization for initial commands to run at startup.
- See keyword-commands for how keyword commands are processed.
- See ld for many ways to control the top-level loop.
- See compilation for a discussion of set-compiler-enabled and
other compiler-related utilities.
- For useful reader macros `#!', `#.', and `#u', see sharp-bang-reader, see sharp-dot-reader, and see sharp-u-reader.
- To save and use an ACL2 executable, see ACL2-as-standalone-program
and see save-exec.
- For utilities related to timing, see time$, see with-prover-time-limit, see with-prover-step-limit, and see set-prover-step-limit.
- To query and manage the database, see history (which discusses
many useful utilities, such as :pbt and :pl), and
see dead-events.
- See add-include-book-dir, add-include-book-dir!, and project-dir-alist for linking keyword for :dir argument of ld
and include-book.
- See rebuild for a fast way to load a file without waiting for
proofs.
- For parallel certification, see books-certification for use of the
-j option of `make'; also see provisional-certification.
Some relatively less common events
Output and its control (see io for additional information)
On proving termination for definitions:
Proof debugging and output control:
Program debugging:
- See break$ to cause an immediate Lisp break.
- See break-on-error to break when encountering a hard or soft error
caused by ACL2.
- See disassemble$ to disassemble a function.
- See print-gv to print a form whose evaluation caused a guard
violation.
- See profile to turn on profiling for one function.
- See trace$ and see open-trace-file to trace function
evaluations, possibly sending trace output to a file.
- See wet to evaluate a form and print a subsequent error
trace.
Programming and evaluation idioms, support, utilities
(also see programming for more utilities, e.g., random$).
- See arrays and See defstobj for introductions
to ACL2 arrays and single-threaded objects (stobjs), respectively, each of
which provides efficient destructive operations in an applicative setting.
Also see with-local-stobj for a way to create local stobjs.
- See assert$ to cause a hard error if the given test is false.
- See canonical-pathname to obtain the true absolute filename, with
soft links resolved.
- See case-match for a utility providing pattern matching and
destructuring.
- See defpun to define a tail-recursive function symbol.
- See ec-call to execute a call in the ACL2 logic instead of raw
Lisp.
- See er to print an error message and ``cause an error''.
- See flet and macrolet to provide local binding of function
and macro names.
- See gc$ to invoke the garbage collector.
- See mbe to attach code for execution.
- See mv-list to convert a multiple-value result to a
single-value list.
- See mv? to return one or more values.
- For non-executable code, see defun-nx and see non-exec.
- See prog2$ and see progn$ to execute two or more forms and
return the value of the last one.
- See programming-with-state for how to program using the von
Neumannesque ACL2 state object.
- See top-level to evaluate a top-level form as a function body.
- See with-guard-checking to suppress or enable guard-checking for a
form.
- For ways to fake access to the state see wormhole, see with-local-state, see cw, see cw!, see printing-to-strings, see observation-cw, and (dangerous!) see with-live-state.
Connecting with the underlying host Lisp, and doing other evil:
- See defttag to introduce a trust tag (ttag).
- See defmacro-last to define a macro that returns its last
argument, but with side effects.
- See progn! to evaluate forms that are not necessarily events.
- See return-last to return the last argument, perhaps with side
effects.
- See set-raw-mode to enter or exit ``raw mode,'' a raw Lisp
environment.
- See sys-call, sys-call+, and sys-call* to make a
system call to the host operating system.
Macros and related utilities:
- See defabbrev for a convenient form of macro
definition for simple expansions.
- See macro-args for the formals list of a macro definition (see
defmacro).
- See make-event for a sort of extension of defmacro that
allows access to the state, by evaluating (expanding) a given form and
then evaluate the result of that expansion.
- See trans, see trans!, and see trans1 to print the
macroexpansion of a form.
Additional capabilities:
- See hons-and-memoization for a discussion of the hons-enabled features providing hash cons, function memoization, and
applicative hash tables. In particular, see memoize for efficient
function memoization and see profile for profiling.
- See real for ACL2(r), which supports the real numbers.
- See parallelism for ACL2(p), which supports parallel evaluation
and proof.
Database control and query:
Prover control
- For congruence-based reasoning see defcong, see congruence, see equivalence, see defequiv, and see defrefinement.
- For meta rules and clause processors see meta, see defevaluator, see clause-processor, see define-trusted-clause-processor (for connecting with external tools, such as
SAT solvers), and See extended-metafunctions (for state and
context-sensitive metafunctions).
- For theory control, see theories for detailed information, but in
particular see deftheory, see theory-functions, see in-arithmetic-theory (and see non-linear-arithmetic), and see theory-invariant.
- See hints for a complete list of prover hints, including some of
the more obscure ones such as :restrict, :clause-processor,
:nonlinearp, :backchain-limit-rw, :reorder, and
:backtrack. Also see hints-and-the-waterfall for an explanation
of how hints interact with the ACL2 proof process. For other topics related
to hints, see override-hints, see add-custom-keyword-hint, see
default-hints, and see computed-hints and using-computed-hints.
- See bind-free to bind free-variables of a rewrite or
linear rule.
- See case-split for a utility like force that immediately
splits the top-level goal on the indicated hypothesis.
- See case-split-limitations for a way to the number of cases
produced at once
- See default-backchain-limit to specify the backchain limit for a
rule.
- See force for an identity function used to force a hypothesis.
- See otf-flg for a way to push more than one initial subgoal for
induction.
- See rule-classes to add various kinds of rules to the database,
including more unusual sorts such as :built-in-clause rules and
:induction rules.
- See set-backchain-limit to set the backchain-limit used by the
type-set and rewriting mechanisms.
- See set-body to set an alternate definition body for :expand
hints.
- See set-rewrite-stack-limit to set the rewrite stack depth
used by the rewriter.
- See syntaxp to attach a heuristic filter on a :rewrite, :meta, or :linear rule.
Subtopics
- Set-check-invariant-risk
- Affect certain program-mode updates to stobjs or arrays
- Invariant-risk
- Potential slowdown for program-mode updates to stobjs
or arrays
- Set-register-invariant-risk
- Avoid invariant-risk checking for specified functions
- Program-wrapper
- Avoiding expensive guard checks using program-mode functions
- Set-duplicate-keys-action
- Control action for macro calls with duplicate keyword arguments
