Note-2-7-other
ACL2 Version 2.7 Notes on Miscellaneous Changes
Made several minor documentation improvements. We are
grateful to Eric Smith for suggesting (most of) these.
Improved (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 'prove and 'event are
inhibited, then events are no longer printed on behalf of certify-book, encapsulate, or defstobj. Thanks to Eric Smith
for prompting consideration of such a change.
The following technical change was made to support with-error-trace
and wet (see note-2-7-new-functionality), but may be of interest
to those who do low-level programming using the ACL2 logical world.
The 'unnormalized-body property is now stored not only for functions
defined in :logic mode, but also for functions defined by the
user in :program mode. (:Program mode Functions built into
ACL2 still have their '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
the 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 ACL2-defaults-table as suggested by Eric and Rob, but this
feature didn't work anyhow (see note-2-7-bug-fixes). Incidentally, the
symbols binop-table, add-binop, and remove-binop have all
been added to the list *acl2-exports* (see ACL2-user), add-invisible-fns and remove-invisible-fns have been added to that
list, and set-invisible-fns-alist has been replaced in that list by
set-invisible-fns-table. Function invisible-fns-alistp is no
longer defined and has been removed from *acl2-exports*.
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 functions (with respect to the current
ACL2 logical world). We make a similar requirement on invisible-fns-table.
The 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.
The command :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 mutual-recursion nest.
The defaults for keyword parameters of certify-book have changed.
See note-2-7-bug-fixes, in particular, the discussion there of two
modifications to certify-book.
Technical changes have been made to compress1 and compress2
that should usually be invisible to users. The next paragraph describes them
in detail, only for completeness (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 'acl2-array
property of the array name contains the array list object in its car.
However, previously it was the case that compress1 and compress2 did
not update that 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 defconst in type-set-b.lisp. The new versions of compress1 and
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 car
of 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 elsewhere (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
XEmacs.
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 new macro, value-triple. The two have the same semantics at the
top-level of books, where state is ``live''. However,
value-triple 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 books.
