NOTE-4-2

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 4.2 into the following categories of changes: existing features, new features, heuristic improvements, bug fixes, distributed books, 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

The accumulated-persistence utility can now do finer-grained tracking, providing data for individual hypotheses and the conclusion of a rule. See accumulated-persistence. To try this out, evaluate the form (accumulated-persistence :all); then see accumulated-persistence for a discussion of display options using show-accumulated-persistence. Thanks to Dave Greve for suggesting this new capability and collaborating on its design and implementation.

The defattach utility now permits the use of :program mode functions, though this requires the use of a trust tag (see defttag). See defattach and for discussion of the new capability, see defproxy, which explains how part of this change involves allowing :program mode functions to be declared non-executable.

Redefinition (see ld-redefinition-action) is no longer permitted for functions that have attachments (see defattach). In such cases, the attachment must be removed first, e.g. with (defattach foo nil).

Made small changes to mv-nth and defun-sk in order to permit guard verification of functions introduced with more than one quantified variable in a defun-sk form. The change to mv-nth is to weaken the guard by eliminating the requirement that the second argument satisfy true-listp, and replacing the call of endp in the definition body by a corresponding call of atom. The new definition of mv-nth is thus logically equivalent to the old definition, but with a weaker guard. Thanks to Sol Swords for sending the following example, for which the final verify-guards form had failed but now succeeds.

(defstub foo (a b c) nil)
(defun-sk forall-a-b-foo (c)
   (forall (a b) (foo a b c))
   :witness-dcls ((declare (Xargs :guard t
                                  :verify-guards nil))))
(verify-guards forall-a-b-foo)

The implementations of prog2$, time$, with-prover-time-limit, with-guard-checking, mbe (and must-be-equal), and ec-call have changed. See the discussion below of the new utility, return-last. A consequence is that trace$ is explicitly disallowed for these and related symbols, which formerly could cause hard Lisp errors, because they are now macros. Tracing of return-last is also disallowed. Another consequence is that time$ now prints a more abbreviated message by default, but a version of the old behavior can be obtained with :mintime nil.

The following utilities no longer print an observation about raw-mode transitions: set-raw-mode-on, set-raw-mode-on!, set-raw-mode, and set-raw-mode-off. Thanks to Jared Davis for suggestion this change in the case of include-book (which proved awkward to restrict to that case).

The system function translate-and-test now permits its LAMBDA form to refer to the variable WORLD, which is bound to the current ACL2 logical world.

Modified abort handling to avoid talking about an interrupt when the error was caused by a Lisp error rather than an interrupt.

The value of the constant *acl2-exports*, which is still a list, has been extended significantly, though only with the addition of symbols that one might reasonably have expected all along to belong to this list. A new distributed book, books/misc/check-acl2-exports.lisp, checks (at certification time) that no documented constant, macro, or function symbol in the "ACL2" package has been accidentally omitted from *acl2-exports*. Thanks to Dave Greve for helpful discussions related to this change.

Improved the built-in `untranslate' functions to produce let* expressions when appropriate (more to help with tools that call untranslate and the like, than to help with proof output).

The utility redo-flat now works for certify-book failures, just as it continues to work for failures of encapsulate and progn.

The following only affects users who use trust tags to add to list values of either of the state global variables program-fns-with-raw-code or logic-fns-with-raw-code. For functions that belong to either of the above two lists, trace$ will supply a default value of :fncall to keyword :notinline, to avoid discarding raw-Lisp code for the function.

The guard of the macro intern has been strengthened so that its second argument may no longer be either the symbol *main-lisp-package-name* or the string "COMMON-LISP". That change supports another change, namely that the following symbols in the "COMMON-LISP" package are no longer allowed into ACL2: symbols in that package that are not members of the list constant *common-lisp-symbols-from-main-lisp-package* yet are imported into the "COMMON-LISP" package from another package. See pkg-imports and see symbol-package-name. To see why we made that change, consider for example the following theorem, which ACL2 was able to prove when the host Lisp is GCL.

(let ((x "ALLOCATE") (y 'car))
  (implies (and (stringp x)
                (symbolp y)
                (equal (symbol-package-name y)
                       "COMMON-LISP"))
           (equal (symbol-package-name (intern-in-package-of-symbol x y))
                  "SYSTEM")))

The axioms introduced by defpkg have changed. See the discussion of pkg-imports under ``NEW FEATURES'' below.

The error message for free variables (e.g., in definition bodies and guards) now supplies additional information when there are governing IF conditions. Thanks to Jared Davis for requesting this enhancement and collaborating in its design.

The command :redef- now turns off redefinition.

Improved proof output in the case of a :clause-processor hint that proves the goal, so that the clause-processor function name is printed.

The proof-checker command `then' now stops at the first failure (if any).

It is no longer permitted to submit definitions in :logic mode for merely part of an existing mutual-recursion event. Such an action left the user in an odd state and seemed a potential soundness hole.

The function break$ is now in :logic mode. Thanks to Jared Davis for requesting this enhancement.

The macro verify-termination now provides clearer output in the case that it is redundant. More important perhaps, as a courtesy it now causes an error when applied to a constrained function, since presumably such an application was unintended (as the constrained function could never have been in :program mode). Note that if one desires different behavior, one can create one's own version of verify-termination (but with a different name).

Improved the guards for the following functions, often weakening them, to reflect more precisely the requirements for calling eq: alist-difference-eq, intersection-eq, intersection1-eq, intersectp-eq, not-in-domain-eq, set-difference-assoc-eq, set-equalp-eq, and union-eq. Thanks to Jared Davis for pointing out this issue for intersectp-eq.

(CCL only) Made a change that can reduce the size of a compiled file produced by certify-book when the host Lisp is CCL, by discarding source information (for example, discarding local events).

NEW FEATURES

See the discussion above about new statistics that can be gathered by the accumulated-persistence utility.

A new hint, :instructions, allows use of the proof-checker at the level of hints to the prover. Thanks to Pete Manolios for requesting this feature (in 2001!). See instructions.

(For system hackers) There are new versions of system functions translate1 and translate, namely translate1-cmp and translate-cmp respectively, that do not take or return state. See the Essay on Context-message Pairs for relevant information. Thanks to David Rager for collaborating on this enhancement.

A new utility, return-last, is now the unique ACL2 function that can pass back a multiple value result from one of its arguments. Thus, now the following are macros whose calls ultimately expand to calls of return-last: prog2$, time$, with-prover-time-limit, with-guard-checking, mbe (and must-be-equal), and ec-call. With an active trust tag, an advanced user can now write code that has side effects in raw Lisp; see return-last. Thanks to Jared Davis for requesting this feature.

A new function, pkg-imports, specifies the list of symbols imported into a given package. The axioms for defpkg have been strengthened, taking advantage of this function. Now one can prove theorems using ACL2 that we believe could not previously be proved using ACL2, for example the following.

(equal (symbol-package-name (intern-in-package-of-symbol str t))
       (symbol-package-name (intern-in-package-of-symbol str nil)))

Added function no-duplicatesp-eq.

Added a new hint keyword, :backchain-limit-rw, to control the level of backchaining for rewrite, meta, and linear rules. This overrides, for the current goal and (as with :in-theory hints) descendent goals, the default backchain-limit (see set-backchain-limit). Thanks to Jared Davis for requesting this feature.

Support is now provided for creating and certifying books that do not depend on trust tags, in the case that the only use of trust tags is during make-event expansion. See set-write-acl2x. Thanks to Sol Swords for reporting a couple of bugs in a preliminary implementation.

Function (file-write-date$ filename state) has been added, giving the write date of the given file.

See forward-chaining-reports for how to get new reports on the forward chaining activity occurring in your proof attempts. Thanks to Dave Greve for inspiring the addition of this utility.

It is now possible to use ACL2's printing utilities to return strings, by opening output channels to the keyword :STRING rather than to filenames. See io. Thanks to Jared Davis for a helpful conversation that led us to add this feature.

HEURISTIC IMPROVEMENTS

We have slightly improved the handling of :forward-chaining rules that contain free variables. Formerly, such rules might fire only once, when the first match for a free variable is discovered, and would not fire again even if subsequent forward chaining made available another match. This made it difficult to predict whether a rule with free variables would fire or not, depending as it did on the order in which newly derived conclusions were added. The new handling is a little slower but more predictable. Thanks to Dave Greve for sending a helpful example that led us to consider making such an improvement.

We have slightly improved the so-called ``type-set'' heuristics to work a bit harder on terms of the form (rec term), where rec is a so-called ``compound-recognizer'' function, that is, a function with a corresponding enabled :compound-recognizer rule. Thanks to Jared Davis for sending a helpful example (found, in essence, in the modified function type-set-rec, source file type-set-b.lisp).

We made three heuristic improvements in the way contexts (so-called ``type-alists'') are computed from goals (``clauses''). Although these changes did not noticeably affect timing results for the ACL2 regression suite, they can be very helpful for goals with many hypotheses. Thanks to Dave Greve for sending a useful example (one where we found a goal with 233 hypotheses!).

The algorithm for substituting alists into terms was modified. This change is unlikely to affect many users, but in one example it resulted in a speed-up of about 21%. Thanks to Dave Greve for supplying that example.

Sped up include-book a bit by memoizing checksums of symbols. (This change pertains to ``normal'' ACL2 only, not the hons version (see hons-and-memoization, where such memoization already occurred.) We found about a 23% speed-up on an example from Dave Greve.

Made a small change to the algorithm used to prove hypotheses of :type-prescription rules (ACL2 source function type-set-relieve-hyps). One change avoids a linear walk through the context (the ``type-alist'' structure), while the other could avoid storing unnecessary forced assumptions (into the so-called ``tag-tree'').

BUG FIXES

Fixed a long-standing soundness bug caused by the interaction of forced hypotheses with destructor elimination. The fix was to avoid using forcing when building the context (so-called ``type-alist'') when the goal is considered for destructor elimination; those who are interested can see a discussion in source function eliminate-destructors-clause1, which includes a proof of nil that no longer succeeds. A similar fix was made for generalization, though we have not exploited the previous code to prove nil in that case.

Fixed a bug that allowed book certification to ignore skip-proofs around encapsulate events. Thus, a book could contain an event of the form (skip-proofs (encapsulate ...)), and a call of certify-book on that book could succeed even without supplying keyword :skip-proofs-okp t. This bug was introduced in Version 3.5 (May, 2009).

Fixed a bug that could occur when including a book that attempts to redefine a function as a macro, or vice-versa. (For details of the issue, see the comment in the definition of variable *hcomp-fn-macro-restore-ht* in source file other-events.lisp.)

(Windows only) Fixed handling of the Windows drive so that an executable image saved on one machine can be used on another, even with a different drive. Thanks to Harsh Raju Chamarthi for reporting this issue and doing a lot of testing and collaboration to help us get this right.

Made a change to avoid possible low-level errors, such as bus errors, when quitting ACL2 by calling good-bye or its synonyms. This was occurring in CCL, and we are grateful to Gary Byers for helping us find the source of those errors (which basically was that ACL2 was attempting to quit while already in the process of quitting).

Fixed a bug in with-guard-checking, which was being ignored in function bodies.

Fixed a bug in top-level, which was not reverting the logical world when an error resulted from evaluation of the given form. Thanks to Jared Davis for bringing this bug to our attention.

Fixed a long-standing bug (back through Version 2.7) that was discarding changes to the connected book directory (see cbd) when exiting and then re-entering the top-level ACL2 loop (with lp).

In some host Lisps, it has been possible to be in a situation where it is impossible to interrupt checkpoint printing during the summary. We had thought this solved when the host Lisp was CCL, but Sol Swords sent us an example (for which we are grateful) illustrating that this behavior could occur. This has been fixed.

Fixed a bug in a proof obligation generated for :meta and :clause-processor rules, that the guard on the metafunction or clause-processor function, fn, holds under suitable assumptions. Those assumptions include not only that the first argument of fn satisfies pseudo-termp, but also that all stobj inputs satisfy the corresponding stobj recognizer predicates. We had erroneously considered stobj outputs of fn instead of stobj inputs. Thanks to Sol Swords for bringing this bug to our attention with a simple example, and correctly pointing us to the bug in our code.

Fixed the following bugs in defattach. We hadn't always been applying the full functional substitution when generating guard proof obligations. We had been able to hit an assertion when reattaching to more than one function. Attachment was permitted in the case of an untouchable function (see remove-untouchable). Finally, the guard proof obligation could fail in the case that the two functions have different formal parameter lists, as in the following example.

(encapsulate
 ((foo (x) x :guard (symbolp x)))
 (local (defun foo (x) x)))
(defun bar (x2)
  (declare (xargs :guard (symbolp x2)))
  x2)
(defattach foo bar)

Fixed a raw Lisp error that could be caused by including a book using make-event to define a function symbol in a locally-introduced package. An example appears in a comment in ACL2 source function write-expansion-file.

Made a change that can prevent an error near the end of book certification when the underlying Host Lisp is Allegro Common Lisp, in the case that environment variable ACL2_SYSTEM_BOOKS has been set to the name of a directory with a parent that is a soft link. Thanks to Dave Greve for supplying an example to led us to this fix, which involves avoiding Allegro CL's implementation of the Common Lisp function, truename.

Fixed a bug that was failing to substitute fully using bindings of free variables in forced hypotheses. A related change is that instead of binding such a free variable to a new variable of the form ???-Y, the new variable is now of the form UNBOUND-FREE-Y.

Fixed a bug that could inhibit the printing of certain theory warnings (and probably, in the other direction, cause inappropriate such printing).

We eliminated excessive "Raw-mode" warnings about add-include-book-dir that could be generated by the use of raw-mode during include-book. Thanks to Dave Greve for bringing this issue to our attention.

Fixed the printing of results from forms within an encapsulate, so that they are abbreviated according to the ld-evisc-tuple.

It is now possible to evaluate stobj-related forms after evaluating :set-guard-checking :none or :set-guard-checking nil, even in cases where such evaluation formerly caused a guard violation due to a bug in ACL2. Here is an example of an error that no longer occurs.

ACL2 !>(defstobj st fld)

Summary
Form:  ( DEFSTOBJ ST ...)
Rules: NIL
Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
 ST
ACL2 !>(set-guard-checking :none)

Turning off guard checking entirely.  To allow execution in raw Lisp
for functions with guards other than T, while continuing to mask guard
violations, :SET-GUARD-CHECKING NIL.  See :DOC set-guard-checking.

ACL2 >(fld st)


ACL2 Error in TOP-LEVEL:  The guard for the function call (FLD ST),
which is (STP ST), is violated by the arguments in the call (FLD ST).
[... etc. ...]

Fixed a bug in which the wrong attachment could be made when the same function has an attachment in a book and another in the certification world of that book (possibly even built into ACL2), if the load of a compiled file is aborted because a sub-book's compiled file is missing. The bug has been present since the time that defattach was added (Version_4.0). An example may be found in a comment in the deflabel for note-4-2 (ACL2 source file ld.lisp).

The :doc and related utilities now cause a clean error when provided other than a symbol. Thanks to Jared Davis for pointing out the raw Lisp error that had occurred in such cases.

It had been the case that in raw-mode (see set-raw-mode), it was possible to confuse include-book when including a book in a directory different from the current directory. This has been fixed. Thanks to Hanbing Liu for bringing this problem to our attention with a small example.

NEW AND UPDATED BOOKS AND RELATED INFRASTRUCTURE

Many changes have been made to the distributed books, thanks to an active ACL2 community. You can contribute books and obtain updates between ACL2 releases by visiting the acl2-books project web page, http://acl2-books.googlecode.com/.

There is new Makefile support for certifying just some of the distributed books. See book-makefiles, in particular discussion of the variable ACL2_BOOK_DIRS. Thanks to Sandip Ray for requesting this enhancement.

The documentation for make-event now points to a new book, books/make-event/defrule.lisp, that shows how make-event can be used to do macroexpansion before generating events. Thanks to Carl Eastlund for useful interaction on the acl2-help mailing list that led us to add this example.

EMACS SUPPORT

Incorporated a version of changes from Jared Davis to the control-t f emacs utility (distributed file emacs/emacs-acl2.el), so that one can fill a format string from anywhere within the string.

EXPERIMENTAL VERSIONS

We refrain from listing changes here to experimental versions, other than an enhancement to the HONS version that can reduce sizes of certificate files, by applying hons-copy to introduce structure sharing (ACL2 source function make-certificate-file1).