Major Section: NOTE-2-7
Made several minor documentation improvements. We are grateful to Eric Smith for suggesting (most of) these.
(show-bdd) (see bdd) to give more useful feedback when there
are ``leaf'' terms not known to be Boolean.
Sped up processing of large mutual-recursion nests. In one large example the speedup was roughly two orders of magnitude.
Modified event printing so that if both
are inhibited, then events are no longer printed on behalf of
to Eric Smith for prompting consideration of such a change.
The following technical change was made to support
wet (see note-2-7-new-functionality), but may be of interest to those
who do low-level programming using the ACL2 logical
'unnormalized-body property is now stored not only for functions defined
logic mode, but also for functions defined by the user in
program mode. (
:Program mode Functions built into ACL2 still
'unnormalized-body property omitted, in order to save space.)
The handling of ``invisible'' functions for purposes of controlling rewriting
(see loop-stopper) has been moved to a new table; see invisible-fns-table.
Macros that access and modify this table are called
...-invisible-fns-table'' in place of their former names,
...-invisible-fns-alist.'' This feature was formerly implemented in
acl2-defaults-table, which prevented a book from exporting lists of
invisible functions intended to work with the rewrite rules developed in
the book. Thanks to Eric Smith and Rob Sumners for suggesting this change.
See set-invisible-fns-table (formerly
set-invisible-fns-alist), and also
see add-invisible-fns and see remove-invisible-fns, which provides ways to
incrementally add to and remove from this table, respectively. The handling
of printing binary function call nests using macros
(See add-binop) has also been moved out of the
suggested by Eric and Rob, but this feature didn't work anyhow
(see note-2-7-bug-fixes). Incidentally, the symbols
remove-binop have all been added to the list
*acl2-exports* (see acl2-user),
remove-invisible-fns have been added to that list, and
set-invisible-fns-alist has been replaced in that list by
invisible-fns-alistp is no
longer defined and has been removed from
We now enforce the stated restriction on the pairings in
macro-aliases-table (see macro-aliases-table), namely, that it
associates names of macros with names of funcions (with respect to the
current ACL2 logical world). We make a similar requirement on
theory-invariant event has been modified so that the default action
is an error rather than a warning. Thanks to Eric Smith for suggesting this
change. Also, the value returned upon successful execution of a
theory-invariant event is now the key.
Proof output that reports destructor elimination no longer uses the word ``generalizing''. This small change may help in browsing proof output, since now ``generaliz'' takes you to true uses of generalization. Thanks to Matyas Sustik for suggesting such a change.
pl now prints an abbreviated controller-alist for
definition rules. Formerly the output from
:pl could be
overwhelming when the supplied function was part of a large
The defaults for keyword parameters of
certify-book have changed.
See note-2-7-bug-fixes, in particular, the discussion there of two
Technical changes have been made to
should usually be invisible to users. The next paragraph describes them in
detail, only for competeness (i.e., that description can be ignored by most
users). But first, here is an example showing an effect on users. The slow
array warning was not there previously. Notice that the warning only arises
if the event form is changed. The solution is to be sure that redundant
defconst forms are syntactically identical.
ACL2 !>(defconst *a* (compress1 'demo '((:header :dimensions (5) :maximum-length 15 :default uninitialized :name demo) (1 . one) (0 . zero)))) Summary Form: ( DEFCONST *A* ...) Rules: NIL Warnings: None Time: 0.00 seconds (prove: 0.00, print: 0.00, other: 0.00) *A* ACL2 !>(aref1 'demo *a* 0) ZERO ACL2 !>(defconst *a* (compress1 'demo '((:header :dimensions (5) :maximum-length 15 :default uninitialized :name demo) (1 . one) (0 . zero)))) This event is redundant. See :DOC redundant-events. Summary Form: ( DEFCONST *A* ...) Rules: NIL Warnings: None Time: 0.00 seconds (prove: 0.00, print: 0.00, other: 0.00) :REDUNDANT ACL2 !>(aref1 'demo *a* 0) ZERO ACL2 !>(defconst *a* (compress1 'demo '((:header :dimensions (5) :maximum-length 15 :default uninitialized :name demo) (0 . zero) (1 . one)))) This event is redundant. See :DOC redundant-events. Summary Form: ( DEFCONST *A* ...) Rules: NIL Warnings: None Time: 0.00 seconds (prove: 0.00, print: 0.00, other: 0.00) :REDUNDANT ACL2 !>(aref1 'demo *a* 0) ********************************************************** Slow Array Access! A call of AREF1 on an array named DEMO is being executed slowly. See :DOC slow-array-warning ********************************************************** ZERO ACL2 !>
As before, the von Neumann structure stored in the
of the array name contains the array list object in its
previously it was the case that
compress2 did not
car when its new value would be equal to its old value. This
was done largely in support of some type-set tables defined using
type-set-b.lisp. The new versions of
compress2 are simpler in that no such exception is made in the case
of equal lists, although instead the entire compression process is
short-circuited when the input array list object is
eq to the
'acl2-array property. This change was made because the equality
test was causing a ``slow array access'' warning to be printed in rare cases
during proofs, as described elswhere (see note-2-7-bug-fixes).
We no longer distribute documentation specific to Lucid Emacs. The Info
documentation in directory
doc/EMACS/ works well both for Gnu Emacs and
A little-advertised macro,
value, has long been allowed for top-level
forms in books; see embedded-event-form. This has been replaced by a
value-triple. The two have the same semantics at the
top-level of books, where
state is ``live''. However,
should be used at the top-level of a book, while
value should be used in
function definitions (as before). This change eliminates a warning put out
by the Allegro Common Lisp compiler for top-level
value forms in