ACL2 Version 1.8 (May, 1995) Notes
See note-1-8-update for yet more recent changes.
Guards have been eliminated from the ACL2 logic. A summary is
contained in this brief note. Also see defun-mode and see set-guard-checking.
Guards may be included in defuns as usual but are ignored
from the perspective of admission to the logic: functions must terminate on
As in Nqthm, primitive functions, e.g., + and car,
logically default unexpected arguments to convenient values. Thus, (+ 'abc
3) is 3 and (car 'abc) is nil. See programming, and
see the documentation for the individual primitive functions.
In contrast to earlier versions of ACL2, Version 1.8 logical functions are
executed at Nqthm speeds even when guards have not been verified. In
versions before 1.8, such functions were interpreted by ACL2.
Colors have been eliminated. Two ``defun-modes'' are supported,
:program and :logic. Roughly speaking, :program does what :red used to do, namely, allow you to prototype
functions for execution without any proof burdens. :Logic mode
does what :blue used to do, namely, allow you to add a new definitional
axiom to the logic. A global default-defun-mode is comparable to the
old default color. The system comes up in :logic mode. To
change the global defun-mode, type :program or
:logic at the top-level. To specify the defun-mode of a
defun locally use
(declare (xargs :mode mode)).
The prompt has changed. The initial prompt, indicating
:logic mode, is
If you change to :program mode the prompt becomes
Guards can be seen as having either of two roles: (a) they are a
specification device allowing you to characterize the kinds of inputs a
function ``should'' have, or (b) they are an efficiency device allowing
logically defined functions to be executed directly in Common Lisp. If a
guard is specified, as with xargs :guard, then it
is ``verified'' at defun-time (unless you also specify xargs
:verify-guards nil). Guard verification means what it always has:
the input guard is shown to imply the guards on all subroutines
in the body. If the guards of a function are verified, then a call of
the function on inputs satisfying the guard can be computed directly by
Common Lisp. Thus, verifying the guards on your functions will allow
them to execute more efficiently. But it does not affect their logical
behavior and since you will automatically get Nqthm speeds on unverified
logical definitions, most users will probably use guards either as a
specification device or only use them when execution efficiency is extremely
Given the presence of guards in the system, two issues are
unavoidable. Are guards verified as part of the defun process?
And are guards checked when terms are evaluated? We answer both of
those questions below.
Roughly speaking, in its initial state the system will try to verify
the guards of a defun if a :guard is supplied in
the xargs and will not try otherwise. However, guard
verification in defun can be inhibited ``locally'' by supplying the
xargs :verify-guards nil. ``Global'' inhibition can
be obtained via the :set-verify-guards-eagerness. If you do not
use the :guard xargs, you will not need to think about
We now turn to the evaluation of expressions. Even if your functions
contain no guards, the primitive functions do and hence you have the
choice: when you submit an expression for evaluation do you mean for guards to be checked at runtime or not? Put another way, do you mean for the
expression to be evaluated in Common Lisp (if possible) or in the logic?
Note: If Common Lisp delivers an answer, it will be the same as in the logic,
but it might be erroneous to execute the form in Common Lisp. For example,
should (car 'abc) cause a guard violation error or return
The top-level ACL2 loop has a variable which controls which sense of
execution is provided. To turn ``guard checking on,'' by which we mean
that guards are checked at runtime, execute the top-level form
:set-guard-checking t. To turn it off, do :set-guard-checking nil.
The status of this variable is reflected in the prompt.
means guard checking is on and
means guard checking is off. The exclamation mark can be thought of
as ``barring'' certain computations. The absence of the mark suggests the
absence of error messages or unbarred access to the logical axioms. Thus, for
ACL2 !>(car 'abc)
will signal an error, while
ACL2 >(car 'abc)
will return nil.
Note that whether or not guards are checked at runtime is
independent of whether you are operating in :program mode or
:logic mode and whether theorems are being proved or not.
(Although it must be added that functions defined in :program
mode cannot help but check their guards because no logical definition
Version 1.8 permits the verification of the guards of theorems, thus
insuring that all instances of the theorem will evaluate without error in
Common Lisp. To verify the guards of a theorem named name execute
If a theorem's guards have been verified, the theorem is guaranteed
to evaluate without error to non-nil in Common Lisp (provided resource
errors do not arise).
Caveat about verify-guards: implies is a function symbol,
so in the term (implies p q), p cannot be assumed true when q
is evaluated; they are both evaluated ``outside.'' Hence, you cannot
generally verify the guards on a theorem if implies is used to
state the hypotheses. Use if instead. In a future version of ACL2,
implies will likely be a macro.
See sum-list-example.lisp for a nice example of the use of Version 1.8.
This is roughly the same as the documentation for guard-example.
We have removed the capability to do ``old-style-forcing'' as existed
before Version 1.5. See note-1-5.
NOTE: Some low level details have, of course, changed. One such change is
that there are no longer two distinct type prescriptions stored when a
function is admitted with its guards verified. So for example, the
type prescription rune for binary-append is now
while in Versions 1.7 and earlier, there were two such runes:
(:type-prescription binary-append . 1)
(:type-prescription binary-append . 2)
Nqthm-style forcing on linear arithmetic assumptions is no longer
executed when forcing is disabled.
Functional instantiation now benefits from a trick also used in Nqthm: once
a constraint generated by a :functional-instance lemma instance
(see lemma-instance) has been proved on behalf of a successful event,
it will not have to be re-proved on behalf of a later event.
1+ and 1- are now macros in the logic, not functions.
Hence, for example, it is ``safe'' to use them on left-hand sides of rewrite
rules, without invoking the common warning about the presence of nonrecursive
A new documentation section file-reading-example illustrates
how to process forms in a file.
A new proof-builder command forwardchain has been added; see
It is now possible to use quantifiers. See defun-sk and see defchoose.
There is a new event set-inhibit-warnings, which allows the user to
turn off warnings of various types. see set-inhibit-warnings.
An unsoundness relating encapsulate and :functional-instance
hints has been remedied, with a few small effects visible at the user
level. The main observable effect is that defaxiom and non-local
include-book events are no longer allowed in the scope of any
encapsulate event that has a non-empty signature.
When certify-book is called, we now require that the default defun-mode (see default-defun-mode) be :logic. On a
related note, the default defun-mode is irrelevant to include-book; the mode is always set to :logic initially, though
it may be changed within the book and reverts to its original value at the
conclusion of the include-book. A bug in include-book
prevented it from acting this way even though the documentation said
The documentation has been substantially improved. A new section
``Programming'' contains documentation of many useful functions
provided by ACL2; see programming. Also, the documentation has
been ``marked up'' extensively. Thus in particular, users of Mosaic will find
many links in the documentation.
The symbols force, mv-nth, and acl2-count have been
added to the list *acl2-exports*.
We now permit most names from the main Lisp package to be used as names,
except for names that define functions, macros, or constants. See name.
We have changed the list of imports from the Common Lisp package to ACL2,
i.e., the list *common-lisp-symbols-from-main-lisp-package*, to be
exactly those external symbols of the Common Lisp package as specified by the
draft Common Lisp standard. In order to accommodate this change, we have
renamed some ACL2 functions as shown below, but these and other ramifications
of this change should be transparent to most ACL2 users.
warning --> warning$
print-object --> print-object$
Proof trees are no longer enabled by default. To start them up,
We have added the capability of building smaller images. The easiest way
to do this on a Unix (trademark of AT&T) system is: make small.
Here we will put some less important changes, additions, and so on.
We have added definitions for the Common Lisp function position
(for the test eql), as well as corresponding versions position-equal and position-eq that use tests equal and
eq, respectively. See position, see position-equal, and
The defthm event rational-listp-implies-rationalp-car no
We fixed a bug in the hint mechanism that applied :by, :cases,
and :use hints to the first induction goal when the prover
reverted to proving the original goal by induction.
We fixed a bug in the handling of (set-irrelevant-formals-ok
In support of removing the old-style forcing capability, we deleted the
initialization of state global old-style-forcing and deleted the
definitions of recover-assumptions, recover-assumptions-from-goal,
remove-assumptions1, remove-assumptions, and
split-on-assumptions, and we renamed split-on-assumptions1 to
The special value 'none in the proof-builder commands
claim and = has been replaced by :none.
A bug in the handling of hints by subgoals has been fixed. For
example, formerly a :do-not hint could be ``erased'' by a :use hint
on a subgoal. Thanks go to Art Flatau for noticing the bug.
The functions weak-termp and weak-term-listp have been deleted,
and their calls have been replaced by corresponding calls of pseudo-termp and pseudo-term-listp. The notion of pseudo-termp
has been slightly strengthened by requiring that terms of the form (quote
...) have length 2.
Performance has been improved in various ways. At the prover level,
backchaining through the recognizer alist has been eliminated in order to
significantly speed up ACL2's rewriter. Among the other prover changes (of
which there are several, all technical): we no longer clausify the input term
when a proof is interrupted in favor of inducting on the input term. At the
io level, we have improved performance somewhat by suitable
declarations and proclamations. These include technical modifications to the
macros mv and mv-let, and introduction of a macro the-mv
analogous to the macro the but for forms returning multiple
The function spaces now takes an extra argument, the current
A bug in the proof-builder equiv command was fixed.
The function intersectp has been deleted, because it was essentially
duplicated by the function intersectp-equal.
We now proclaim functions in AKCL and GCL before compiling books.
This should result in somewhat increased speed.
The function repeat has been eliminated; use make-list
The proof-builder command expand has been fixed so that it
eliminates let (lambda) expressions when one would expect it to.
A new primitive function, mv-nth, has been introduced. Mv-nth is equivalent to nth and is used in place of nth in
the translation of mv-let expressions. This allows the user to
control the simplification of mv-let expressions without affecting how
nth is treated. In that spirit, the rewriter has been modified so
that certain mv-nth expressions, namely those produced in the
translation of (mv-let (a b c)(mv x y z) p), are given special
A minor bug in untranslate has been fixed, which for example will fix
the printing of conjunctions.
Translate now takes a logicp argument, which indicates whether it
enforces the restriction that :program mode functions do not
occur in the result.
The modified version of trace provided by ACL2, for use in raw Lisp,
has been modified so that the lisp special variable *trace-alist* has a
slightly different functionality. This alist associates, using eq,
symbols with the print representations of their values. For example,
initially *trace-alist* is a one-element list containing the pair
(cons 'state '|*the-live-state*|). Thus, one may cons the pair (cons
'*foo* "It's a FOO!") on to *trace-alist*; then until *foo* is
defined, this change will have no effect, but after for example
(defconst *foo* 17)
then trace will print 17 as "It's a FOO!".
Trace also traces the corresponding logic function.
Proof-tree display has been improved slightly in the case of
successful proofs and certain event failures.
The function positive-integer-log2 has been deleted.
The macro skip-proofs now prints a warning message when it is
encountered in the context of an encapsulate event or a book. See
Some functions related to the-fn and wormhole1 now have defun-mode :program, but this change is almost certain to be
inconsequential to all users.