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 all arguments.
As in Nqthm, primitive functions, e.g., + and car,
logically default unexpected arguments to convenient values. Thus,
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,
(declare (xargs :mode mode)).
The prompt has changed. The initial prompt, indicating
If you change to
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
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
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,
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
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 example
ACL2 !>(car 'abc)
will signal an error, while
ACL2 >(car 'abc)
Note that whether or not guards are checked at runtime is
independent of whether you are operating in
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
If a theorem's guards have been verified, the theorem is guaranteed
to evaluate without error to non-
Caveat about verify-guards: implies is a function symbol,
so in the term
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
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 function symbols.
A new documentation section file-reading-example illustrates how to process forms in a file.
A new proof-builder command
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
When certify-book is called, we now require that the default defun-mode (see default-defun-mode) be
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
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
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 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 see position-eq.
The defthm event
We fixed a bug in the hint mechanism that applied
We fixed a bug in the handling of
In support of removing the old-style forcing capability, we deleted the
initialization of state global
The special value
A bug in the handling of hints by subgoals has been fixed. For
example, formerly a
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
A bug in the proof-builder
We now proclaim functions in AKCL and GCL before compiling books. This should result in somewhat increased speed.
The proof-builder command
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
A minor bug in
The modified version of
(defconst *foo* 17)
Proof-tree display has been improved slightly in the case of successful proofs and certain event failures.
The macro skip-proofs now prints a warning message when it is encountered in the context of an encapsulate event or a book. See skip-proofs.
Some functions related to