Major Section: RELEASE-NOTES
See note8-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 all arguments.
As in Nqthm, primitive functions, e.g.,
default unexpected arguments to convenient values. Thus,
(+ 'abc 3)
(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,
logic. Roughly speaking,
program does what
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
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
ACL2 !>If you change to
programmode 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
it is ``verified'' at defun-time (unless you also specify
: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 important.
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
and will not try otherwise. However, guard verification in
can be inhibited ``locally'' by supplying the
nil. ``Global'' inhibition can be obtained via
set-verify-guards-eagerness. If you do not use the
xargs, you will not need to think about guard
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
The status of this variable is reflected in the prompt.
ACL2 !>means guard checking is on and
ACL2 >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 example
ACL2 !>(car 'abc)will signal an error, while
ACL2 >(car 'abc)will return
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
mode cannot help but check their guards because no logical
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 the event
(verify-guards name).If a theorem's guards have been verified, the theorem is guaranteed to evaluate without error to non-
nilin Common Lisp (provided resource errors do not arise).
implies is a function symbol, so in the
(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
if instead. In a future version of ACL2,
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 note5.
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
(:type-prescription binary-append)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
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- 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 function symbols.
A new documentation section file-reading-example illustrates how to process forms in a file.
A new proof-checker command
forwardchain has been added;
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.
An unsoundness relating
hints has been remedied, with a few small effects visible at the
user level. The main observable effect is that
include-book events are no longer allowed in the scope
encapsulate event that has a non-empty signature.
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
mode is always set to
logic initially, though it may be changed
within the book and reverts to its original value at the conclusion
include-book. A bug in
include-book prevented it from
acting this way even though the documentation said otherwise.
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.
acl2-count have been added
to the list
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
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:
Here we will put some less important changes, additions, and so on.
We have added definitions for the Common Lisp function
(for the test
eql), as well as corresponding versions
position-eq that use tests
eq, respectively. See position, see position-equal,
and see position-eq.
We fixed a bug in the hint mechanism that applied
: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
In support of removing the old-style forcing capability, we deleted
the initialization of state global
old-style-forcing and deleted the
and we renamed
The special value
'none in the proof-checker commands
has been replaced by
A bug in the handling of hints by subgoals has been fixed. For
example, formerly a
:do-not hint could be ``erased'' by a
on a subgoal. Thanks go to Art Flatau for noticing the bug.
weak-term-listp have been
deleted, and their calls have been replaced by corresponding calls
pseudo-term-listp. The notion of
pseudo-termp has been slightly strenthened 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-let, and introduction of a macro
the-mv analogous to the
the but for forms returning multiple values.
spaces now takes an extra argument, the current column.
A bug in the proof-checker
equiv command was fixed.
intersectp has been deleted, because it was
essentially duplicated by the function
We now proclaim functions in AKCL and GCL before compiling books. This should result in somewhat increased speed.
repeat has been eliminated; use
The proof-checker command
expand has been fixed so that it
let (lambda) expressions when one would expect it to.
A new primitive function,
mv-nth, has been introduced.
is equivalent to
nth and is used in place of
nth in the
mv-let expressions. This allows the user to
control the simplification of
mv-let expressions without
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 treatment.
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
has a slightly different functionality. This alist associates,
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
*foo* is defined, this change will have no effect, but
after for example
(defconst *foo* 17)then
"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.
positive-integer-log2 has been deleted.
skip-proofs now prints a warning message when it is
encountered in the context of an
encapsulate event or a book.
Some functions related to
wormhole1 now have
program, but this change is almost certain to
be inconsequential to all users.