Note-2-8-other
ACL2 Version 2.8 Notes on Miscellaneous Changes
Execution of table events has been sped up in many cases by
avoiding excessive consing.
ACL2 now warns if :rewrite (or :definition) rules
contain free variables on the right-hand side. Thanks to Dave Greve for
raising this issue.
Emacs file emacs/emacs-acl2.el has been updated to better comprehend
the notion of the ``ACL2 shell'', which is the buffer to which ACL2 forms are
written by commands defined in the above file. Thus, command control-t e
has been modified always to write to the ACL2 shell (which is "*shell*"
by default), and the following new commands have been defined.
o control-t c
Set the ACL2 shell to the current buffer.
o control-t b
Change to the ACL2 shell.
The commands :pl and :pr may now be given a macro
name that corresponds via the macro-aliases-table to a function name, so
that for example :pl append is treated the same as :pl
binary-append. A more interesting improvement, for :pl only, is that
:pl may now take any term. When :pl is given a term other than a
symbol, it will print all rewrite rules that match that term. Thanks to David
Russinoff, Robert Krug, and Bill Legato for getting this going.
A new function, pkg-witness, returns a symbol in the given
package.
The installation instructions have been updated, for example to give more
guidance on obtaining Lisp implementations and to mention the acl2-help
mailing list.
Jared Davis has suggested some symbols to be added to *acl2-exports*,
and we have done so. Thanks, Jared.
o MFC (used in syntaxp and extended-metafunctions; thanks also to Robert Krug for this one) o ID,
CLAUSE, WORLD, and STABLE-UNDER-SIMPLIFICATIONP (used in computed-hints) o set-default-hints
The command :pe has been improved so that when the event is
inside an included book, the path of included books (from the top-level book
down to the one containing the event) is shown. Thanks to Eric Smith (perhaps
among others) for pointing out the utility of this improvement.
A new release of the rtl library has been included: books/rtl/rel4/.
See the README file in that directory.
