Note-6-5
ACL2 Version 6.5 (August, 2014) Notes
NOTE! New users can ignore these release notes, because the documentation has been updated to reflect all changes that are recorded
here.
Below we roughly organize the changes to ACL2 since Version 6.4 into the
following categories of changes: existing features, new features, heuristic
improvements, bug fixes, changes at the system level, Emacs support, and
experimental versions. Each change is described in just one category, though
of course many changes could be placed in more than one category.
See also note-6-5-books for a summary of changes made to the ACL2
Community Books since ACL2 6.4, including the build system.
Changes to Existing Features
The brr@ command now supports inputs :initial-ttree and
:final-ttree. Thanks to David Rager for a request leading to these
enhancements. See ttree for a discussion of the tag-tree structures
returned for these inputs.
(GCL only) A restriction for structure-sharing (as described in a remark,
``Remark on print-circle-files''; see print-control) involving GCL has
been removed, since this is no longer required for the latest GCL
versions (2.6.8 and 2.6.10). Thanks to Jared Davis and Camm Maguire for
useful discussions and this GCL improvement.
The keyword commands :exit and :quit are disabled inside brr, in order to avoid accidental exits from ACL2. Thanks to David Rager for
suggesting such a change.
For calls of make-event made during the include-book phase
of certify-book, keyword :check-expansion no longer causes
evaluation of the first argument of make-event; rather, the value of
:check-expansion is simply used as the expansion. Thanks to Sol Swords
for suggesting this change, which made it reasonable to ignore such
make-event forms when determining the ``rolling back'' before that
include-book phase, as described in the next section.
The form (reset-prehistory nil) now is a no-op if state global
'skip-reset-prehistory has a non-nil value. Thanks to Sol
Swords for requesting this feature (in support of infrastructure for
certifying the community-books).
The output from :pr, :pr!, :pl, and
:show-bodies has been tweaked. Thanks to a suggestion from Ben
Selfridge, such output now shows the hypotheses (the Hyps field) above
the left-hand side and right-hand side of a rewrite rule (Lhs and
Rhs, respectively). The Equiv field has also been moved up before
the Lhs field in such output for rewrite rules, and this field has been
added for elim rules. Finally, the Hyps field now appears above
the Term field in such output for type-prescription rules.
Rules of class :linear may now be monitored. Thanks to
David Rager for requesting this enhancement.
When forcing (see force) is applied, we now always see the
appropriate executable-counterpart rune, (:executable-counterpart force), in
the proof output and summary; this hadn't previously been the case. Thanks to
Robert Krug for bringing this issue to our attention.
The default value for the :write-port keyword argument of certify-book is now t, as was already claimed by the documentation.
Thus, a .port file will be written when a book is certified, making it
more likely that a subsequent include-book will complete without error
even if the book has been modified without recertification. Note that a
change by Sol Swords to the build system for the community-books now
sets an environment variable to guarantee that write-port is true,
independent of this change. On a related note: the unadvertised environment
variable ACL2_WRITE_PORT is now handled more appropriately, by interning
its upcased argument into the ACL2 package.
The following changes can make it easier to include books that are
uncertified or have corrupted compiled files. Thanks to Sol Swords for
sending helpful, relevant examples and for subsequent discussions helping to
lead to these changes.
- It is no longer illegal to call set-compiler-enabled within books. See compilation, which shows how to do this in order to avoid
loading the compiled file not only for a book specified by include-book but also for all books included under that book. Also see compilation for an analogous utility, (set-port-file-enabled nil state),
to avoid loading .port files. (For background on .port files, see
uncertified-books).
- In situations where it is legal to include an uncertified book (typically,
any time other than during certify-book, ACL2 nonetheless could fail
to do so when an error occurred while reading a certificate file. ACL2
can now instead include the book successfully as an uncertified book.
- When hard raw Lisp errors occur during loading of compiled files on behalf
of an include-book event, that event can now complete successfully
much as though the compiled file were simply missing.
(SBCL only) The function setenv$ is now supported in SBCL, which
had been the one supported host Lisp for which setenv$ had not been
supported. Thanks to Jared Davis for pointing the way to this
improvement.
Built-in equality-variants have been modified in order to support
suitable guard-checking. For example, evaluation of the form (member-eq 3
'(4 5)), or equivalently, (member 3 '(4 5) :test 'eq), had produced a
value of nil, but now we get what one should have expected: a guard
violation (since member-eq is intended to compare symbols). Thanks to
Yan Peng for raising a question on the acl2-help mailing list that led us to
make this improvement.
When the :pe command is supplied the macro alias for a
function symbol (see macro-aliases-table), the system will now print
events not only for the macro symbol but also for the corresponding
function symbol. Thanks to Cuong Chau, Jared Davis, Shilpi Goel, Sol Swords,
and Warren Hunt for requesting this enhancement.
Some evaluations of forms (mbe :logic L :exec E) are more efficient or
avoid guard violations, by evaluation of the :exec form (E) instead
of the :logic form (L). If the mbe call is in a
:program mode function definition, the :exec code will be
evaluated, where unlike before, this is true even when guard-checking is
:all or :none (see set-guard-checking). If the mbe call
is in a :logic mode function definition, the change is that the
:exec code will be evaluated when there is a superior call of a
:program mode function, except when guard-checking is :all or
:none or in a couple of technical cases (see a comment in the source code
for constant **1*-as-raw* [formerly *mbe-as-exec*] for details).
This use of :exec code had been defeated when the superior :program
mode function had an ``invariant-risk'' of making ill-guarded stobj updates.
However, there is no change in the case of safe-mode, which is used during
evaluation of defconst, value-triple, and defpkg
forms, and during macroexpansion: the :logic and :exec forms are
still both evaluated and checked for equality. Thanks to Jared Davis for
reporting this issue and for helpful chats about it. For more information,
see the comment about ``mbe and invariant-risk'' in the form (defxdoc
note-6-5 ...) in community-books file
books/system/doc/acl2-doc.lisp.
The utility save-exec has a new (optional) keyword argument,
:init-forms, which specifies a list of forms to evaluate when first
entering the ACL2 read-eval-print loop, lp. Thanks to Jared Davis for
requesting this enhancement.
New Features
A defstobj event may now include the keyword argument
:non-memoizable. When its value if t, then for ACL2(h) builds (see
hons-and-memoization), code will run somewhat faster. In a little test
doing just reads and writes to a stobj array in ACL2(h), it took 26% less time
when the stobj to be written was introduced by defstobj using
:non-memoizable t. Thanks to Warren Hunt for requesting this
feature and helping to develop the test.
See set-print-base-radix for a utility that may be preferable to
set-print-base, since it essentially calls set-print-radix
automatically. Thanks to David Rager, Shilpi Goel, and David Hardin for
participating in an acl2-help mailing list discussion that motivated this
feature.
Heuristic Improvements
One of the steps performed by certify-book has traditionally been
to check for local incompatibilities (see local-incompatibility) after
admitting all the events in the book. This step involved rolling back the
logical world to what it was at the start of certification, and then
including the book (see include-book). As an optimization, we now
avoid rolling back the world more than necessary; see certify-book,
specifically the discussion of Step 3. We thank Sol Swords for requesting
this optimization and for making a suggestion that improved it, pertaining to
make-event (described above). We also thank Jared Davis for alerting
us to an issue that turned out to be caused by a bug in our initial
implementation. Sol has reported a nearly 20% reduction in time for
certifying a certain large collection of books.
The test for redundancy of encapsulate events has been made
more efficient. Also, while the criterion itself remains unchanged, the
documentation has been made more accurate; see redundant-encapsulate.
We observed more than a 2% reduction in time for the ``everything'' regression
target, but we observed more than 23% of the time eliminated for the form
(time$ (include-book "doc/top" :dir :system)) after building the
documentation. Thanks to David Rager for bringing that particular book to our
attention, as one that took a long time to include.
The function pairlis$ is now tail-recursive, hence potentially more
efficient. More precisely, its definition for the logic remains unchanged,
but using mbe, for execution it calls a new tail-recursive function,
pairlis$-tailrec. Thanks to Jared Davis for requesting this
improvement.
Linear arithmetic has been strengthened slightly so that immediately
after simplification has ``settled down'' (see hints-and-the-waterfall), the unrewritten conclusion of a :linear rule may be used when normally this would not be the case. Thanks to
Robert Krug for reminding us of examples we had encountered that could benefit
from some such a change, and for pointing us to some relevant source code.
This improvement generally causes an extra pass through the simplifier; hence
we have observed approximately a 2% slowdown in the regression suite. Note
that machinery is now in place for installing additional ``desperation
heuristics''; perhaps the ACL2 community will have some to suggest.
Bug Fixes
We fixed a soundness bug in how the tau-system processed calls of
if. Thanks to Dmitry Nadezhin for reporting this bug by sending a simple
example that exploited it to prove nil. To see that example, see the
comment about ``tau soundness bug'' in the form (defxdoc note-6-5 ...) in
community-books file books/system/doc/acl2-doc.lisp.
We fixed a soundness bug for nested stobjs (see stobj-let).
In the case of a stobj producer variable that is not a child stobj, it had
been possible to update that stobj without returning it. Thanks to Sol Swords
for reporting this bug and providing a corresponding proof of nil, which
is included in a comment in the form (defxdoc note-6-5 ...) in community-books file books/system/doc/acl2-doc.lisp.)
We fixed a soundness bug in the case of a stobj with a field that is
a resizable array of stobjs. Thanks to Sol Swords for sending a proof of
nil exploiting this bug, together with some helpful analysis attributing
the bug to a mistake in the generated logical definition of the corresponding
resize function. (His example is included in a comment in the form
(defxdoc note-6-5 ...) in community-books file
books/system/doc/acl2-doc.lisp.)
(ACL2(h) only) We fixed a soundness bug involving the interaction of stobj-let and memoize, which thus is only a bug in ACL2(h) (see hons-and-memoization), not in ACL2. The fix was to add code to
stobj-let that clears the memoization table for the parent stobj if any
child stobj is updated. An example proof of nil before this fix may be
found in the ACL2 source file translate.lisp, in a comment in the
function stobj-let-fn-raw.
(Allegro CL and CMUCL only) We fixed bugs in function princ$ when
invoked in an ACL2 image with Allegro CL or CMUCL as the host Lisp
implementation. In Allegro CL, when printing a complex number in base 16,
lower case characters were produced, for example printing #C(c d) instead
of the characters predicted by the axioms, namely #C(C D). In some
recent versions of CMUCL, after executing the forms (set-print-base 16
state) and (set-print-case :downcase state), hex digits were printed in
lower case, unlike other host Lisps and contrary to the ACL2 axioms: for
example, 1000 base 10 was printed as 3e8 rather than as predicted by the
ACL2 axioms, 3E8. Thanks to Jared Davis for bringing these bugs to our
attention, and also for pointing out excessive printing of a big note about
such printing in Allegro CL. We now avoid that note altogether, which had
warned that printing numbers in base 16 can be slow for Allegro CL. In fact,
that performance issue has been eliminated: for example, after evaluating
(defconst *c* (expt 2 200000)) and (set-print-base 16 state), the
form (time$ (pprogn (princ$ *c* *standard-co* state) state)) reports
taking about 3 seconds before the change but about 1/100 seconds after the
change. Thanks to David Margolies of Franz Inc. for passing along a remark
from a colleague that showed how to make this improvement.
The utility sys-call+ can now only be called if there is an active
trust-tag, which is the restriction that was already in place for
sys-call. This plugs a potential soundness hole.
We have made several system functions untouchable (see remove-untouchable), in order to prevent soundness bugs. We thank Jared
Davis and Sol Swords for sending us an example that used a call of one of
these functions to prove nil. We have placed that example into a comment
in Community Books file system/doc/acl2-doc.lisp, form (defxdoc
note-6-5 ...).
The brr command, :wonp, had not been installed for use after
:eval even though this was claimed in the documentation (see brr-commands). This has been fixed. Thanks to David Rager for bringing this
issue to our attention.
Fixed a bug in make-event that could cause include-book to
fail with a bogus message about ``the set of ttags permitted
in the current context.'' Thanks to Sol Swords and Anna Slobodova for
reporting this bug, and to Sol for sending a small example that illustrated
the problem.
Fixed a bug that was wrongly disallowing certain calls of exported
functions for abstract stobjs (see defabsstobj). Thanks to Sol Swords
for reporting this bug, supplying an example illustrating the bug, and
suggesting a nice fix. A slight variant of his example is included in a
comment in Community Books file system/doc/acl2-doc.lisp, form
(defxdoc note-6-5 ...).
When a macro symbol mac was a macro-alias for a function symbol
f (see macro-aliases-table), then the form (verify-guards+
mac) caused an error when encountered while including an uncertified book.
This problem has been fixed. Thanks to Jared Davis for pointing out the
problem and sending a simple example to illustrate it. Technical Note: the
actual problem was that verify-guards+ generates a call of make-event with an :expansion? argument, and that argument needed to be
ignored (as it now is, after the fix) when including an uncertified book.
The walkabout utility could cause hard Lisp errors when the current
package is other than "ACL2". This has been fixed. Thanks to Sol
Swords for bringing this bug to our attention and suggesting a fix.
Changes at the System Level
(SBCL only) Fixed the executable script generated for SBCL so that
SBCL_HOME is set to the SBCL obj/sbcl-home/ directory if it exists,
since that fix seems needed for some recent versions of SBCL (1.1.14 in
particular).
File GNUmakefile in the ACL2 sources directory wasn't passing the
value of shell variable ACL2 from target certify-books-fresh to
target certify-books, and similarly for target
books/system/doc/render-doc.cert (invoked by target DOC). This has
been fixed. We thank Jared Davis and Camm Maguire for helpful
discussions.
The "make DOC" command was not completing correctly when variable
ACL2 was not set. Also, for host Lisp CMUCL at least, it stalled at the
terminal unless a quit command was issued twice (as ACL2 was stuck without
exiting). Those problems have been resolved. Thanks to Jim Ward for bringing
these issues to our attention
Improved the error message when encountering an illegal comma while reading
input (i.e., for a comma not within a suitable nesting of backquotes). Thanks
to Jared Davis for bringing this issue to our attention and for a helpful
discussion.
(GCL only) Arranged for state global 'tmp-dir to be set to GCL's
si::*tmp-dir*, even on Windows; this may be important for compilation on
Windows. Thanks to Camm Maguire for pointing out the need to set
'tmp-dir for ACL2 built on GCL on mingw.
(GCL only) Now, gc$ may be called with no arguments, in which case
the missing argument for system::gc is t.
EMACS Support
Improvements to the ACL2-Doc browser include the following.
- A new `w' command displays the topic name in the minibuffer, together
with the manual name (ACL2+Books Manual or ACL2 User's Manual).
- Improved the `control-t .' command so that the default topic is
selected just as in acl2-doc mode. (Technically: the same syntax table is
used for `control-t .' as is used in the acl2-doc buffer for that
command and the `g' command.)
- Improved the search commands so that the display doesn't move when the
next occurrence is already displayed on the screen.
- Eliminated the deprecated commands `Control-x a A',
`Control-x a a', and `Control-t G'.
Experimental/Alternate Versions
For ACL2(r), Ruben Gamboa found a bug in constraints for functions
introduced with defun-std, and also kindly provided a fix, which has been
incorporated.
Modified ACL2(hp) so that two system functions that had been unmemoized when turning on waterfall-parallelism —
fchecksum-obj and expansion-alist-pkg-names-memoize — now
remain memoized. This can greatly improve performance when using ACL2(hp)
with waterfall-parallelism on, in particular community book
books/system/doc/render-doc-combined.lisp.
Made miscellaneous small improvements to ACL2(h).
The utilities hons-shrink-alist and hons-shrink-alist! have
essentially been renamed to fast-alist-fork and fast-alist-fork!, respectively. The old names are deprecated but remain as
macros that are macro-aliases for the respective new names (see macro-aliases-table). New utilities, fast-alist-clean and fast-alist-clean! are similar to the above but take just one argument and, if
it is a fast alist, associates the result with the hash table link of that
argument. Thanks to Jared Davis for providing a concrete proposal, together
with the new names, for what had been only a concept.
Subtopics
- Note-6-5-books
- Release notes for the ACL2 Community Books for ACL2 6.5 (August
2014).
