NOTE-4-3

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, changes at the system level and to 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

Significant changes have been made for list-processing primitives such as member and assoc; see equality-variants. In summary: instead of separate functions based on eq, eql, and equal, there is essentially just one function, which is based on equal; the eq and eql variants are logically just the equal variant. For example, member-eq and member are macros that generate corresponding calls of member-equal in the logic, although in raw Lisp they will execute using tests eq and eql, respectively. References to any of these in logical contexts such as theories are now references to the function based on equal; for example, the hint :in-theory (disable member) is completely equivalent to the hint :in-theory (disable member-equal). Distributed books have been modified as necessary to accommodate this change. While the need for such changes was relatively infrequent, changes were for example needed in contexts where terms are manipulated directly; for example, defevaluator needs to mention member-equal rather than member, just as it was already the case to mention, say, binary-append rather than append. Again, see equality-variants for more information about equality variants.

A few improvements were made in support of the modified treatment of equality variants discussed above. The changes include the following.

o We now allow the use of macro aliases (see macro-aliases-table in :trigger-fns of rules (see rule-classes).

o We now remove so-called ``guard holders'' (including calls of return-last, hence of mbe) in :trigger-terms of rules.

o We also remove guard holders in formulas of :congruence and type-prescription rules.

o Macros union-eq and intersection-eq can now take any positive number of arguments, and union-eq can take zero arguments. (Thanks to Jared Davis for requesting this enhancement.) The same can be said for new macros union$ and intersection$, respectively.

o A few changes were made to built-in theorems from source file axioms.lisp, in particular disabling :type-prescription rule consp-assoc-equal (formerly two enabled rules, consp-assoc-eq and consp-assoc) but adding this theorem as a :forward-chaining rule, and similarly for true-list-listp-forward-to-true-listp-assoc-equal (and eliminating rule true-list-listp-forward-to-true-listp-assoc-eq; and disabling rule true-listp-cadr-assoc-eq-for-open-channels-p. Also, theorem all-boundp-preserves-assoc has been renamed to all-boundp-preserves-assoc-equal and also strengthened.

o Some guards were slightly improved (logically weaker or the same).

Improved get-output-stream-string$ to allow for a context and to do genuine error printing instead of using cw. See io.

Added the symbols flet and with-local-stobj to *acl2-exports*.

A small change was made to the processing of more than one :guard declaration for the same function. In particular, a guard of t is essentially ignored.

Attachments are now allowed during evaluation of the first argument of prog2$ even in contexts (such as proofs) during which the use of attachments is normally prohibited. More generally, the second of the three arguments of return-last has this property, except in the case of mbe (or related macros like mbe1), where the exec argument may provide the value. Thanks to Sol Swords for useful discussions leading us to implement this enhancement.

The restriction has been removed that prohibited the use of mbe inside encapsulate events with a non-empty signature. This restriction was introduced in Version 3.4, but has not been necessary since Version 4.0, when we first started disallowing guard verification for functions introduced non-locally inside such encapsulate events.

We weakened the checks involving common ancestors for evaluator and meta (and clause-processor) functions (see evaluator-restrictions) so that except in the mbe case, the next-to-last argument of return-last is not considered. Thanks to Sol Swords for bringing this issue to our attention.

The macro append no longer requires at least two arguments. Thanks to Dave Greve for requesting this enhancement.

(Mostly for system hackers) Now, break-on-error breaks at a more appropriate (earlier) time for certain system functions that do not return state, such as translate11. Thanks to David Rager for requesting this improvement.

Show-accumulated-persistence may take a new argument, :runes, which simply causes an alphabetical list of runes to be printed out.

Improved trace$ so that :entry, :exit, and :cond forms may reference state even if the function being traced does not include state as a formal.

The system function acl2x-expansion-alist now takes a second argument, namely state. This change allows for more flexibility in the sorts of attachments that can be made to this function (see defattach). Thanks to Jared Davis and Sol Swords for requesting this enhancement and providing a preliminary implementation.

An obscure proof-checker change, unlikely to affect users, replaces the state global variables erp, val, print-macroexpansion-flg, and print-prompt-and-instr-flg by pc-erp, pc-val, pc-print-macroexpansion-flg, and pc-print-prompt-and-instr-flg, respectively.

State globals fmt-hard-right-margin and fmt-soft-right-margin are now untouchable (see set-fmt-hard-right-margin and see push-untouchable). If you bind these state globals with state-global-let*, then you will need to do so with appropriate setters to restore their values, for example as follows.

  (state-global-let*
   ((fmt-hard-right-margin 500 set-fmt-hard-right-margin)
    (fmt-soft-right-margin 480 set-fmt-soft-right-margin))
   ...)

The error message has been improved for the case of evaluating an undefined function that has an attachment (see defattach). Thanks to Jared Davis for sending the following example, which illustrates the additional part of the message.

  ACL2 !>(defstub foo (x) t)
  [[... output omitted ...]]
  ACL2 !>(defattach foo identity)
  [[... output omitted ...]]
  ACL2 !>(defconst *x* (foo 3))


  ACL2 Error in ( DEFCONST *X* ...):  ACL2 cannot ev the call of undefined
  function FOO on argument list:

  (3)

  Note that because of logical considerations, attachments (including
  IDENTITY) must not be called in this context.

  [[... additional output omitted ...]]

The directory string supplied to add-include-book-dir no longer must terminate with the `/' character, as had been required in some Lisp implementations. Thanks to Sol Swords for bringing this issue to our attention.

We no longer print induction schemes with gag-mode; use :pso if you want to see them. Thanks to Dave Greve for this suggestion.

It is now legal to supply a constant for a stobj array dimension. See defstobj. Thanks to Warren Hunt for requesting this enhancement.

We cleaned up a few issues with defpkg.

o It is no longer illegal to submit a defpkg form in raw-mode (see set-raw-mode). Thanks to Jun Sawada for reporting an example in which an include-book form submitted in raw-mode caused an error because of a `hidden' defpkg form (see hidden-defpkg). There will no longer be an error in such cases.

o It had been the case that locally including a book could make it possible to use a package defined by that book. Consider for example the following book, foo.lisp.

(in-package "ACL2")
(local (include-book "arithmetic/top" :dir :system))

After certifying this book, it had been possible to admit the following events in a new session.

(include-book "foo")
(defconst acl2-asg::*foo* 3)
(defconst *c* 'acl2-asg::xyz)

In Version_4.3, neither of these defconst events is admitted.

o A hard Lisp error is now avoided that had been possible in rare cases when including books with hidden packages (see hidden-defpkg). An example may be found in a comment in the deflabel for note-4-3 (in ACL2 source file ld.lisp).

The undocumented (but sometimes useful) functions packn1 and packn are now guard-verified :logic mode functions. Thanks to Sandip Ray for requesting this enhancement.

It had been the case that when including a book, functions defined in the book's certification world (that is, in its portcullis commands) were typically not given compiled code. That has been fixed.

The commands :pl and :pl2 have been improved, primarily by printing information for more rule classes. See pl and see pl2. See also the item below about the new proof-checker command, show-type-prescriptions.

NEW FEATURES

New macros mv?-let and mv? extend the funtionality of mv-let and mv (respectively) to the case of a single value.

Macro with-local-state is available for system programmers who wish bind state locally, essentially using with-local-stobj. But this should only be done with extreme care, and it requires an active trust tag; see with-local-state.

Formatted printing functions now have analogues that print to strings and do not take an output channel or state as arguments. See printing-to-strings.

The system function ancestors-check is now available for verified modification by users, i.e., attachment using (defattach ancestors-check <your_function>). Thanks to Robert Krug for providing the necessary proof support, which we modified only in small ways.

New macros, observation-cw and warning$-cw, provide formatted printing of observations and warnings (respectively) without state. Thanks to Harsh Raju Chamarthi and David Rager for requests leading to these utilities. Observation-cw is now used in some of the distributed books (thanks to Robert Krug for useful interaction for that).

The proof-checker command type-alist (see proof-checker-commands) now takes an optional third argument that causes the production of forward-chaining reports (see forward-chaining-reports). Thanks to Dave Greve for requesting such an enhancement.

The reports generated by forward-chaining, forward-chaining-reports, have been changed to indicate when a conclusion reached by forward chaining is REDUNDANT with respect to the type information already known. Thanks to Dave Greve for suggesting this enhancement.

The utility with-prover-time-limit is now legal for events (see embedded-event-form). For example, the following is now legal.

(encapsulate
 ()
 (with-prover-time-limit 
  2
  (defthm append-assoc
    (equal (append (append x y) z)
           (append x (append y z))))))

The new utility with-prover-step-limit is analogous to the utility with-prover-time-limit, but counts ``prover steps'' rather than checking for time elapsed. See with-prover-step-limit. Also see set-prover-step-limit to provide a default step-limit. Note that just as with-prover-time-limit may now be used to create events, as discussed just above, with-prover-step-limit may also be used to create events. Thanks to Carl Eastlund for requesting support for step-limits.

The macro progn$ is analogous to prog2$, but allows an arbitrary number of arguments. For example:

ACL2 !>:trans1 (progn$ (f1 x) (f2 x) (f3 x))
 (PROG2$ (F1 X) (PROG2$ (F2 X) (F3 X)))
ACL2 !>

The macro defattach may now be supplied the argument :skip-checks :cycles. In this case, as with argument :skip-checks t, a trust tag is reuired (see defttag), and no logical claims are made. The effect is to avoid the usual check that the extended ancestor relation has no cycles (see defattach). Thanks to Dave Greve for requesting this feature.

You can now limit the printing of subgoal names when using :set-gag-mode :goals. See set-print-clause-ids. Thanks to Karl Hoech for a suggestion leading to this enhancement.

A new proof-checker command, show-type-prescriptions, or st for short, provides information about :type-prescription rules that match a given term. Thanks to Dave Greve for requesting this enhancement. See also the item above about related improvements to commands :pl and :pl2.

HEURISTIC IMPROVEMENTS

ACL2 now avoids some repeated attempts to rewrite hypotheses of rewrite rules. See set-rw-cache-state for a discussion of this behavior and how to avoid it. The default behavior has been observed to reduce by 11% the overall time required to complete a regression. Here are the directories that had the top three time decreases and top three time increases, shown in seconds.

  -368 coi/gacc (1064 down to 696: decrease of 35%)
  -220 workshops/1999/ste (664 down to 444: decrease of 33%)
  -148 unicode (331 down to 183: decrease of 45%)
  ....
    +7 workshops/2002/cowles-flat/support (229 up to 236: increase of 3%)
    +8 workshops/1999/ivy/ivy-v2/ivy-sources (508 up to 516: increase of 2%)
   +12 workshops/2009/hardin/deque-stobj (78 up to 91: increase of 17%)

The so-called ``ancestors check,'' which is used to limit backchaining, has been strengthened so that two calls of equal are considered the same even if their arguments appear in the opposite order. Thanks to Robert Krug for providing an implementation and a useful discussion.

The check for irrelevant-formals in processing of defuns has been made more efficient. Thanks to Eric Smith for reporting this issue in 2001 (!) and thanks to Warren Hunt for recently sending an example. For that example, we have seen the time for the irrelevant-formals check reduced from about 10 seconds to about 0.04 seconds.

(GCL only) The macro mv has been modified so that certain fixnum boxing can be avoided.

(Allegro CL only) We have set to nil four Allegro CL variables that otherwise enable storing of certain source information (for details, see the discussion of ``cross-referencing'' in ACL2 source file acl2-init.lisp). As a result of this change we have about a 6% speedup on the regression suite, but a 27% time reduction on an example that includes a lot of books.

Exhaustive matching for the case of free-variables has been extended to type-prescription rules, in analogy to the default setting :match-free :all already in place for rewrite, linear, and forward-chaining rules. See free-variables-type-prescription. Thanks to Dave Greve for requesting this enhancement.

BUG FIXES

A soundness bug was fixed in some raw-Lisp code implementing the function, take. Thanks to Sol Swords for pointing out this bug with (essentially) the following proof of nil.

(defthmd take-1-nil-logic
  (equal (take 1 nil) '(nil))
  :hints(("Goal" :in-theory (disable (take)))))
(thm nil :hints (("Goal" :use take-1-nil-logic)))

Calls of mbe in ``safe-mode'' situations -- i.e., during evaluation of defconst, value-triple, and defpkg forms, and during macroexpansion -- are now guard-checked. Thus, in these situations both the :logic and :exec forms will be evaluated, with an error if the results are not equal. Formerly, only the :logic form was evaluated, which was a soundness bug that could be exploited to prove nil. For a such a proof and a bit of further explanation, see the example at the top of the comments for (deflabel note-4-3 ..) in ACL2 source file ld.lisp.

It had been possible to prove nil by proving the following theorem using ACL2 built on CCL and then proving its negation using ACL2 built on a different host Lisp.

(defthm host-lisp-is-ccl
  (equal (cdr (assoc 'host-lisp *initial-global-table*))
         :ccl)
  :rule-classes nil)

Fixed trace$ for arguments that are stobj accessors or updaters. It also gives an informative error in this case when the accessor or updater is a macro (because the introducing defstobj event specified :inline t).

Avoided a potential error that could occur when no user home directory is located. Our previous solution for Windows simply avoided looking for ACL2 customization files (see acl2-customization) and acl2-init.lsp files in a user's home directory. With this change, we handle such files the same for Windows as for non-Windows systems: we always look for ACL2 customization files (see acl2-customization) and acl2-init.lsp files in a user's home directory, but only if such a directory exists. Thanks to Hanbing Liu for reporting this issue.

(GCL only) Fixed a bug that prevented the use of get-output-stream-string$ when the host Lisp is GCL.

Fixed with-live-state to work properly for executable counterparts (so-called ``*1*'' functions).

Fixed a bug in the error message caused by violating the guard of a macro call.

Fixed a bug in an error message that one could get when calling defattach with argument :skip-checks t to attach to a :program mode function symbol that was introduced with defun. (This is indeed an error, but the message was confusing.) Thanks to Robert Krug for bringing this bug to our attention.

Fixed a bug in the loop-checking done on behalf of defattach, which could miss a loop. For an example, see the comment about loop-checking in the comments for (deflabel note-4-3 ..) in ACL2 source file ld.lisp.

Terms of the form (hide <term>) without free variables could be simplified, contrary to the purpose of hide. This is no longer the case, Thanks to Dave Greve for reporting this issue.

An infinite loop could occur when an error was encountered in a call of wormhole-eval, for example with the following form, and this has been fixed.

(wormhole-eval 'demo
               '(lambda ()
                  (er hard 'my-top "Got an error!"))
               nil)

Fixed a bug in detection of package redefinition. While we have no example demonstrating this as a soundness bug, we cannot rule it out.

Fixed a bug in the message produced by an erroneous call of flet. Thanks to Jared Davis for reporting this bug and sending a helpful example.

For a failed defaxiom or defthm event, we now avoid printing runes that are used only in processing proposed rules to be stored, but not in the proof itself. Thanks to Dave Greve for sending us an example that led us to make this fix.

ACL2 did not reliably enforce the restriction against non-local include-book events inside encapsulate events, as illustrated by the following examples.

; not permitted (as expected)
(encapsulate () (include-book "foo"))

; permitted (as expected)
(encapsulate () (local (include-book "foo")))

; formerly permitted (surprisingly); now, not permitted
(local (encapsulate () (include-book "foo")))

When include-book is given a first argument that is not a string, a more graceful error now occurs, where previously an ugly raw Lisp error had occurred. Thanks to Eric Smith for bringing this bug to our attention.

Fixed a bug in an error message that was printed when an unexpected expression has occurred where a declare form is expected.

(Since all functions are compiled when the host Lisp is CCL or SBCL, the following bug fix did not occur for those host Lisps.) After evaluation of (set-compile-fns t), all defined functions are expected to run with compiled code; but this was not the case for functions exported from an encapsulate event. This has been fixed.

It had been the case that the :puff command was broken for include-book form whose book had been certified in a world with an add-include-book-dir event. This has been fixed.

Evaluation of stobj updaters (see defstobj) may no longer use attachments (see defattach). This is a subtle point that will likely not affect many users. Thanks to Jared Davis for bringing this issue to our attention; a slight variant of his example appears in a comment in ACL2 source function oneify-cltl-code.

It had been the case that even when a stobj creator function was declared to be untouchable (see push-untouchable), a with-local-stobj form based on that same stobj was permitted. Now, such forms are not admitted. Thanks to Jared Davis for a query leading to this fix.

Fixed a buggy message upon guard violations, which was suggesting the use of (set-guard-checking :none) in some cases when guard-checking was already set to :none.

It had been possible to get a hard Lisp error when computing with ec-call in books. The following is an example of such a book, whose certification no longer causes an error.

(in-package "ACL2")
(defun f (x) x)
(defconst *c* (ec-call (f 3)))
(defun g (x) (cons x x))

The command :pl2, and also the proof-checker commands rewrite and show-rewrites (and hence their respective aliases r and sr), now take rule-id arguments that can be :definition runes. These commands dealt with definition rules already, e.g.

:pl2 (append x y) binary-append

:pl2 (append x y) (:definition binary-append)

The following example illustrates a bug in the processing of (admittedly obscure) hints of the form :do-not-induct name, where name is not t, :otf-flg-override, :otf, or nil. In this example, ACL2 had essentially ignored the hint and reverted to prove the original goal by induction, rather than to skip the goal temporarily as is expected for such hints. Thanks to David Rager for a helpful discussion.

(thm (and (equal (append (append x y) z) (append x y z))
          (equal (append (append x2 y2) z2) (append x2 y2 z2)))
     :hints (("Subgoal 1" :do-not-induct some-name)))

Fixed a slight bug in the definitions of built-in theories. For example, in a fresh ACL2 session the value of the following form is nil, but formerly included several :definition runes.

(let ((world (w state)))
  (set-difference-theories (function-theory :here)
                           (function-theory 'ground-zero)))

CHANGES AT THE SYSTEM LEVEL AND TO DISTRIBUTED BOOKS

Many changes have been made to the distributed books, as recorded in svn logs under the `Source' and 'Updates' links at http://acl2-books.googlecode.com/. Here we list some of the more significant changes.

o A large library has been graciously contributed by the formal verification group at Centaur Technology. See books/centaur/ and, in particular, file books/centaur/README, which explains how the library depends on the experimental HONS extension (see hons-and-memoization).

o Among the new books is an illustration of defattach, books/misc/defattach-example.lisp, as well as a variant of defattach that avoids the need for guard verification, books/misc/defattach-bang.lisp.

o Distributed book books/misc/trace1.lisp has been deleted. It had provided slightly more friendly trace output for new users, but distributed book books/misc/trace-star.lisp may be better suited for that purpose.

ACL2 can once again be built on LispWorks (i.e., as the host Lisp), at least with LispWorks 6.0. Thanks to David Rager for useful conversations. Several changes have been made from previous LispWorks-based ACL2 executables:
o ACL2 now starts up in its read-eval-print loop.
o You can save an image with save-exec.
o Multiprocessing is not enabled.
o The stack size is managed using a LispWorks variable that causes the stack to grow as needed.
o When ACL2 is built a script file is written, as is done for other host Lisps. Thus, (assuming that no PREFIX is specified), saved_acl2 is just a small text file that invokes a binary executable, which for Lispworks is saved_acl2.lw.

The HTML documentation no longer has extra newlines in <pre> environments.

Statistics on ACL2 code size may be found in distributed file doc/acl2-code-size.txt. This file and other information can be found in a new documentation topic, about-acl2.

Fixed the build process to pay attention to environment variable ACL2_SYSTEM_BOOKS (which may be supplied as a command-line argument to `make'). An ACL2 executable can thus now be built even when there is no books/ subdirectory if a suitable replacement directory is supplied.

Some warnings from the host Lisp are now suppressed that could formerly appear. For example, the warnings shown below occurs in Version 4.2 using Allegro CL, but not in Version 4.3.

ACL2 !>(progn (set-ignore-ok t)
              (set-irrelevant-formals-ok t)
              (defun bar (x y)
                x))
[[.. output omitted ..]]
 BAR
ACL2 !>:comp bar
; While compiling BAR:
Warning: Variable Y is never used.
; While compiling (LABELS ACL2_*1*_ACL2::BAR ACL2_*1*_ACL2::BAR):
Warning: Variable Y is never used.
 BAR
ACL2 !>

EMACS SUPPORT

The distributed Emacs file emacs/emacs-acl2.el now indents calls of er@par and warning$@par the same way that calls of defun are indented.

EXPERIMENTAL VERSIONS

The parallel version (see parallelism) now supports parallel evaluation of the ``waterfall'' part of the ACL2 prover; see set-waterfall-parallelism. Thanks to David Rager for doing the primary design and implementation work.

A new macro, spec-mv-let, supports speculative and parallel execution in the parallel version, courtesy of David Rager.

Among the enhancements for the HONS version (see hons-and-memoization) are the following.

Memoized functions may now be traced (see trace$). Thanks to Sol Swords for requesting this enhancement.

Memoize-summary and clear-memoize-statistics are now :logic mode functions that return nil. Thanks to Sol Swords for this enhancement.

Memoize is now explicitly illegal for constrained functions. (Already such memoization was ineffective.)

A new keyword argument, :AOKP, controls whether or not to allow memoization to take advantage of attachments; see memoize and for relevant background, see defattach.

Memoize is now illegal by default for :logic mode functions that have not had their guards verified. See memoize (keyword :ideal-okp) and see acl2-defaults-table (key :memoize-ideal-okp) for and explanation of this restriction and how to avoid it.

History commands such as :pe and :pbt now display ``M'' or ``m'' to indicate memoized functions. See pc.