NOTE-6-1

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. Evaluate

(strip-cars (cdr (assoc-equal "system/top" *system-verify-guards-alist*)))

The macro 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 helpful discussions.

Added a field :UNIFY-SUBST to metafunction contexts (see EXTENDED-METAFUNCTIONS), accessed with function mfc-unify-subst. Thanks to Sol Swords for requesting this enhancement.

The functions sys-call and sys-call-status are now guard-verified :logic-mode functions.

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.

The utility print-summary-user has been replaced by finalize-event-user, which is described below. If you previously attached a function to print-summary-user, say my-print-summary-user, 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 files in arithmetic/. Thus, the form (include-book "equalities") attempted to include arithmetic/equalities instead of nonstd/arithmetic/equalities, which caused an error.

We no longer document the use of value :START for 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.

NEW FEATURES

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 print-summary-user.

HEURISTIC IMPROVEMENTS

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.

BUG FIXES

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 (deflabel note-6-1 ...) in ACL2 source file ld.lisp.

We fixed a soundness bug involving system function canonical-pathname 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 ld.lisp.

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 ld.lisp.

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 linearize1).

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 named 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 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: (progn (set-prover-step-limit '(a b))).

CHANGES AT THE SYSTEM LEVEL

The 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 std/lists/rev.lisp, which contains the rule revappend-removal, which may cause some proofs involving 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.

EMACS SUPPORT

EXPERIMENTAL/ALTERNATE VERSIONS

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).