Major Section: RELEASE-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 since Version 6.0 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.
CHANGES TO EXISTING FEATURES
More system functions are in
logic mode, guard-verified.
(strip-cars (cdr (assoc-equal "system/top" *system-verify-guards-alist*)))for the list of functions checked to be guard-verifiable in the community books. Thanks to those who have contributed to this effort, as shown in file headers in directory
system/of the community books.
defund now avoids an error when
:mode :program has been
specified in an
xargs form of a
declare form, for example:
(defund f (x) (declare (xargs :mode :program)) x). It does this by
avoiding the generation of
in-theory events in such cases. Thanks
to David Rager and Jared Davis for requesting such a change, and for ensuing
Added a field
:UNIFY-SUBST to metafunction contexts
(see EXTENDED-METAFUNCTIONS), accessed with function
Thanks to Sol Swords for requesting this enhancement.
sys-call-status are now
It had been the case that if any supporter of a dependent clause processor (see define-trusted-clause-processor) is among the ancestors of a given formula, then it was illegal to apply functional instantiation (see lemma-instance) to that formula. Now, this is illegal only if some such supporter is in the domain of the functional substitution.
The tau system (see tau-system, or if you are unfamiliar with the tau system, see introduction-to-the-tau-system) now allows the user to define and verify functions that compute bounds on arithmetic expressions. See bounders.
print-summary-user has been replaced by
finalize-event-user, which is described below. If you previously
attached a function to
then you can get the effect you had previously as follows.
(defun my-finalize-event-user (state) (declare (xargs :mode :logic :stobjs state)) (prog2$ (my-print-summary-user state) state)) (defattach finalize-event-user my-finalize-event-user)
It had been the case that when you
LD a file, the connected book
directory (see cbd) was set to the canonical pathname of that file's
directory for the duration of the
LD call. This could cause problems,
however, if the file is actually a soft link: an
include-book form in
the book with a relative pathname for the book would be resolved with respect
to the absolute pathname for that link, which is probably not what was
intended. So soft links are no longer followed when computing the above
connected book directory. The following example, which is how we discovered
this problem, may clarify. We attempted to execute the form
(ld "top.lisp") using ACL2(r) (see real) in community books directory
nonstd/arithmetic/, where all of the
.lisp files are soft links to
arithmetic/. Thus, the form
attempted to include
arithmetic/equalities instead of
nonstd/arithmetic/equalities, which caused an error.
We no longer document the use of value
with-prover-step-limit. This value has always been used by the ACL2
implementation and may have semantics that change with new ACL2 versions. If
you have reason to use this value, please contact the ACL2 implementors.
By default, the prover now gives information about case splits. See splitter. Thanks to many ACL2 users, most recently David Rager, for requesting such a capability. Also thanks to David Rager and Jared Davis for helpful discussions, and thanks to Robert Krug for feedback on the initial implementation and documentation that led us to make improvements.
the user to run state-modifying code at the start and end of
events. Thanks to Harsh Raju Chamarthi for requesting these
capabilities. Note that
Several heuristic improvements have been made to the tau system, even if you do not explicitly use the new capability for computing bounds on arithmetic expressions, mentioned above. See tau-system, or if you are unfamiliar with the tau system, see introduction-to-the-tau-system.
A soundness bug has been fixed that exploited the use of expansion files
(see book-compiled-file) together with
defstobj. For an example
illustrating this bug, see the comment about ``Expansion/Defstobj Bug'' in
(deflabel note-6-1 ...) in ACL2 source file
We fixed a soundness bug involving system function
and (most likely) other functions in the former value of constant
*unattachable-primitives*. Thanks to Jared Davis and Sol Swords for
bringing this bug to our attention by way of an example. We include a very
slight variant of that example in a comment within the form
(deflabel note-6-1 ...) in ACL2 source file
There was a soundness bug that allowed attachments to prove
nil in a
consistent logical world involving
defaxiom events. This has
been fixed, by requiring that no function symbol ancestral in a
defaxiom formula is allowed to get an attachment. See defattach, in
particular discussion of ``a restriction based on a notion of a function
symbol syntactically supporting an event'', which concludes with a proof of
nil that is no longer possible.
(ACL2(h) only) We fixed a soundness bug in the interaction of memoization
with congruent stobjs, in cases where the
:congruent-to field of
defstobj was not the canonical representative in the congruence class.
For an example illustrating this bug, see the comment about
``memoize/congruent stobj bug'' in the form
(deflabel note-6-1 ...) in
ACL2 source file
Functions defined by
defstobj had failed to be compiled when certifying
books, except in host Lisps that compile on-the-fly (CCL, SBCL). This has
been fixed for all host Lisps. A related change, probably less significant,
was made for
defabsstobj. Thanks to Sol Swords for reporting bugs that
turned out to be mistakes in a preliminary implementation of this change.
Fixed an assertion error involving linear arithmetic. Thanks to Sol Swords
for sending an example illustrating the bug (now appearing as a comment in
ACL2 source function
Fixed a bug that was breaking the ACL2s build mechanism (see acl2-sedan) by
causing certain needless evaluation of ``hidden
defpkg'' forms in
certificate files when executing a call of
include-book. The bug
could also affect rare error messages arising from ill-formed
certificate files. Thanks to Harsh Raju Chamarthi for bringing this bug
to our attention by sending us an example script of the sort that was
breaking during an ACL2s build.
Fixed handling of pathnames by some low-level code (system function
our-truename) that could cause errors, for example for host-Lisp GCL on
some platforms when environment variable
HOME points to a non-existent
directory. Thanks to Camm Maguire for bringing this issue to our attention
and helping with the debugging.
Fixed a coding bug in generation of stobj resizing functions for a stobj
OLD. The following example illustrates the bug.
(defstobj old (fld :type (array (unsigned-byte 31) (8)) :initially 0 :resizable t)) (resize-fld 10 old) ; The following returned 8 but should have returned 10: (fld-length old)
Fixed a bug in
defabsstobj-missing-events (which macroexpanded
incorrectly). Thanks to Sol Swords for bringing this bug to our attention.
Fixed two bugs in the handling of step-limits. Thanks to Hanbing Liu for
bringing the main such bug to our attention, which was that ACL2 could report
a step-limit violation during
certify-book (in fact, during any
compound event such as a call of
without direct user involvement in managing step-limits
(see set-prover-step-limit and see with-prover-step-limit). The other bug
was that a bad argument to
set-prover-step-limit could result in a raw
Lisp error, for example:
(progn (set-prover-step-limit '(a b))).
CHANGES AT THE SYSTEM LEVEL
books/ directory no longer needs to exist in order to build an ACL2
executable. Thanks to Robert Krug for pointing out that the installation
instructions had suggested that this was already the case.
Many changes have been made to the community books (see community-books).
For example, some community books now include
contains the rule
revappend-removal, which may cause some proofs
revappend to fail where they formerly succeeded, or
vice-versa. When a proof fails that formerly succeeded, it may be useful for
you to look over the runes printed in the event summary.
wormhole-eval is now locked by default; thanks to David
Rager for suggesting this change. But there is a way to avoid the lock;
see wormhole-eval. In particular, the lock is avoided in the
implementations of accumulated-persistence and
forward-chaining-reports, which are not supported in ACL2(p)