ACL2 Version 6.1 (February, 2013) 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
(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. (NOTE added after Version_8.3: The form is now
The macro defund now avoids an error when
Added a field
The functions sys-call and sys-call-status are now guard-verified
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.
(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
We no longer document the use of value
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.
New utilities initialize-event-user and finalize-event-user
allow 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 finalize-event-user replaces
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 the form
We fixed a soundness bug involving system function canonical-pathname and (most likely) other functions in the former value of
There was a soundness bug that allowed attachments to prove
(ACL2(h) only) We fixed a soundness bug in the interaction of memoization
with congruent stobjs, in cases where the
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
Fixed a coding bug in generation of stobj resizing functions for a stobj
(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 encapsulate or progn), even
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:
CHANGES AT THE SYSTEM LEVEL
Many changes have been made to the community-books. For example,
some community books now include
For ACL2(p), 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) (see unsupported-waterfall-parallelism-features).