NOTE-3-4

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 3.3 into changes to existing features, new features, bug fixes, new and updated books, and Emacs support. Each change is described just once, though of course many changes could be placed in more than one category.

CHANGES TO EXISTING FEATURES

Fixed a long-standing potential infinite loop in the rewriter. Thanks to Sol Swords for sending a concise example illustrating the looping behavior. (Those interested in details are welcome to look at the comment about loop behavior in source function rewrite-equal.)

Incorporated a slight strengthening of non-linear arithmetic contributed by Robert Krug (thanks, Robert). With non-linear arithmetic enabled, the problem was essentially that ACL2 made the following ``optimization'': given inequalities (< a u) and (< b v), for positive rational constants a and b terms u and v of which at least one is known to be rational, infer (< (* a b) (* u v)). Without this optimization, however, ACL2 now infers the stronger inequality obtained by direct multiplication of the two given inequalities. To see the effect of this change, submit the event (set-non-linearp t) followed by:

(thm (implies (and (rationalp x) (< 3 x)
                   (rationalp y) (< 4 y))
              (< 0 (+ 12 (* -4 x) (* -3 y) (* x y)))))

The utility set-checkpoint-summary-limit has been modified in several ways: it now takes a single argument (no longer takes state as an argument); a natural number n abbreviates the pair (n . n); the argument is no longer evaluated, but it still optionally may be quoted; and a new value, t, suppresses all printing of the checkpoint summary. Thanks to Jared Davis for suggesting most of these improvements.

There was formerly a restriction on mbe that the :exec argument may not contain a call of mbe. This restriction has been removed, thanks to a request from Jared Davis and Sol Swords. Thanks also to Sandip Ray, who pointed out that this restriction may have been in place in order that defexec can guarantee termination using the :exec code; its documentation has therefore been updated to clarify this situation.

Rules of class :rewrite are now stored by performing certain logical simplifications on the left side of the conclusion: (prog2$ X Y) is replaced by Y, (mbe :logic X :exec Y) is replaced by X (more precisely, the analogous change is made to the generated call of must-be-equal); and (the TYPE X) is replaced by X (again, the change is actually made on the macroexpanded form). Thanks to Jared Davis and Sol Swords for requesting this change. An analogous change has also been made for rules of class :forward-chaining.

The trace$ utility has been reimplemented to work independently of the underlying Lisp trace. It thus works the same for every host Lisp, except as provided by an interface to the underlying host Lisp trace (the :native option). Note that the host Lisp trace continues to be modified for GCL, Allegro CL, and CCL (OpenMCL); see trace. See trace$ for updated detailed documentation on tracing options, many of which are new, for example an :evisc-tuple option that can be set to :no-print if you want the function traced without the usual entry and exit printing. The previous trace$ had some issues, including the following, which have all been fixed. Thanks to Peter Dillinger for assistance in determining desired functionality of the new trace$ and for helping to test it.

Recursive calls were not always shown in the trace for two reasons. (1) Compiler inlining could prevent recursive calls from being shown in the trace, in particular in CCL (OpenMCL). Thanks to Jared Davis and Warren Hunt for pointing out this issue and requesting a fix, and to Bob Boyer and Gary Byers for relevant helpful discussions. (2) ACL2's algorithm for producing executable counterparts prevented tracing of recursive calls even after (set-guard-checking :none). Thanks to Peter Dillinger for requesting a fix.

It was possible to exploit a bug in the interaction of multiple values and trace to prove a contradiction. An example is in a comment in (deflabel note-3-4 ...) in the ACL2 source code.

Certain large structures could cause expensive computations for printing even when a :cond condition was specified and evaluated to nil.

Trace! now suppresses printing of the event summary, and returns the value that would be returned (if there is an active trust tag) by the corresponding call of trace$.

Some bugs have been fixed in the underlying native trace installed by ACL2 for GCL, Allegro CL, and CCL (OpenMCL), including the following. In GCL it had been impossible to use the variable ARGLIST in a :cond expression. In Allegro CL and CCL, a trace$ bug mishandled tracing non-ACL2 functions when directives such as :entry and :exit were supplied. GCL trace now hides the world even when tracing non-ACL2 functions. Tracing in CCL no longer causes a Lisp error when untracing a traced function defined outside the ACL2 loop; for example (trace$ len1) followed by (untrace$ len1) no longer causes an error.

The macro wet has been changed, for the better we think. see wet.

The generation of goals for forcing-rounds has been changed to avoid dropping assumptions formerly deemed ``irrelevant''. (A simple example may be found in a comment in source function unencumber-assumption, source file prove.lisp.) Thanks to Jared Davis for sending us an example that led us to make this change.

Modified the implementation of make-event so that in the certificate of a book, local events arising from make-event forms are elided. For example, if (make-event <form>) expands to (local <expanded-form>), then where the latter had been stored in the certificate, now instead (local (value-triple :ELIDED)) will be stored. Thanks to Eric Smith for requesting this improvement. He has reported that a preliminary version of this improvement shrunk a couple of his .cert files from perhaps 40MB each to about 140K each.

Now, a table event that sets the entire table, (table tbl nil alist :clear), is redundant (see redundant-events) when the supplied alist is equal to the current value of the table. Thanks to Peter Dillinger for requesting this change.

The event constructor progn! now returns the value that is returned by evaluation of its final form if no error occurs, except that it still returns nil if the that final evaluation leaves ACL2 in raw-mode.

:Pso and :psog have been improved so that they show the key checkpoint summary at the end of a failed proof. (For a discussion of key checkpoints, see set-gag-mode.) As a result, a call of set-checkpoint-summary-limit now affects subsequent evaluation of :pso and :psog. In particular, you no longer need to reconstruct a proof (by calling thm or defthm) in order to see key checkpoints that were omitted due to the limit; just call set-checkpoint-summary-limit and then run :pso or :psog.

The proof-checker behaves a little differently under gag-mode. Now, proof-checker commands that call the theorem prover to create new proof-checker goals, such as bash and induct (see proof-checker-commands), will show key checkpoints when in gag-mode. As before, proof-checker commands pso and pso! (and now, also psog) -- see pso, see psog, and see pso! -- can then show the unedited proof log. However, unlike proof attempts done in the ACL2 loop, such proof attempts will not show a summary of key checkpoints at the end, because from a prover perspective, all such goals were considered to be temporarily ``proved'' by giving them ``byes'', to be dispatched by later proof-checker commands.

A little-known feature had been that a measure of 0 was treated as though no measure was given. This has been changed so that now, a measure of nil is treated as though no measure was given.

Expanded *acl2-exports* to include every documented symbol whose name starts with "SET-". Thanks to Jared Davis for remarking that set-debugger-enable was omitted from *acl2-exports*, which led to this change.

The trace mechanism has been improved so that the :native and :multiplicity options can be used together for Lisps that support the trace :exit keyword. These Lisps include GCL and Allegro CL, whose native trace utilities have been modified for ACL2. For SBCL and CCL (OpenMCL), which use the built-in Lisp mechanism for returning multiple values in ACL2 (see mv), the use of :multiplicity with :native remains unnecessary and will be ignored. In support of this change, the modification of native Allegro CL tracing for ACL2 was fixed to handle :exit forms correctly that involve mv.

NEW FEATURES

The command :redef! is just like :redef, but prints a warning rather than doing a query. The old version of :redef! was for system hackers and has been renamed to :redef+.

Introduced a new utility for evaluating a function call using the so-called executable counterpart -- that is, executing the call in the logic rather than in raw Lisp. See ec-call. Thanks to Sol Swords for requesting this utility and participating in its high-level design.

See print-gv for a new utility that assists with debugging guard violations. Thanks to Jared Davis for requesting more tool assistance for debugging guard violations.

Improved the guard violation error message to show the positions of the formals, following to a suggestion of Peter Dillinger.

Added new guard-debug capability to assist in debugging failed attempts at guard verification. See guard-debug. Thanks to Jared Davis for requesting a tool to assist in such debugging and to him, Robert Krug, and Sandip Ray for useful discussions.

New utilities provide the formula to be proved by verify-guards. See verify-guards-formula and see guard-obligation, Thanks to Mark Reitblatt for making a request leading to these utilities. These utilities can be applied to a term, not just an event name; thanks to Peter Dillinger for correspondence that led to this extension.

A new utility causes runes to be printed as lists in proof output from simplification, as is done already in proof summaries. See set-raw-proof-format. Thanks to Jared Davis for requesting this utility.

An experimental capability allows for parallel evaluation. See parallelism. Thanks to David Rager for providing an initial implementation of this capability.

Defined xor in analogy to iff. Thanks to Bob Boyer, Warren Hunt, and Sol Swords for providing this definition.

Improved distributed file doc/write-acl2-html.lisp so that it can now be used to build HTML documentation files for documentation strings in user books. See the comment in the definition of macro acl2::write-html-file at the end of that file. Thanks to Dave Greve and John Powell for requesting this improvement.

It is now possible to specify :hints for non-recursive function definitions (which can be useful when definitions are automatically generated). See set-bogus-defun-hints-ok. Thanks to Sol Swords for requesting such a capability.

Keyword argument :dir is now supported for rebuild just as it has been for ld.

We relaxed the criteria for functional substitutions, so that a function symbol can be bound to a macro symbol that corresponds to a function symbol in the sense of macro-aliases-table. So for example, a functional substitution can now contain the doublet (f +), where previously it would have been required instead to contain (f binary-+).

We now allow arbitrary packages in raw mode (see set-raw-mode) -- thanks to Jared Davis for requesting this enhancement -- and more than that, we allow arbitrary Common Lisp in raw mode. Note however that for arbitrary packages, you need to be in raw mode when the input is read, not just when the input form is evaluated.

Two new keywords are supported by the with-output macro. A :gag-mode keyword argument suppresses some prover output as is done by set-gag-mode. Thanks to Jared Davis for asking for a convenient way to set gag-mode inside a book, in particular perhaps for a single theorem; this keyword provides that capability. A :stack keyword allows sub-events of progn or encapsulate to ``pop'' the effect of a superior with-output call. Thanks to Peter Dillinger for requesting such a feature. See with-output.

The command good-bye and its aliases exit and quit now all take an optional status argument, which provides the Unix exit status for the underlying process. Thanks to Florian Haftmann for sending a query to the ACL2 email list that led to this enhancement.

Keyword commands now work for macros whose argument lists have lambda list keywords. For a macro with a lambda list keyword in its argument list, the corresponding keyword command reads only the minimum number of required arguments. See keyword-commands.

It is now legal to declare variables ignorable in let* forms, as in (let* ((x (+ a b)) ...) (declare (ignorable x)) ...). Thanks to Jared Davis for requesting this enhancement.

Added a warning when more than one hint is supplied explicitly for the same goal. It continues to be the case that only the first hint applicable to a given goal will be applied, as specified in the user-supplied list of :hints followed by the default-hints-table. Thanks to Mark Reitblatt for sending a question that led both to adding this clarification to the documentation and to adding this warning.

You may now use set-non-linear, set-let*-abstraction, set-tainted-ok, and set-ld-skip-proofs in place of their versions ending in ``p''. Thanks to Jared Davis for suggesting consideration of such a change. All ``set-'' utilites now have a version without the final ``p'' (and most do not have a version with the final ``p'').

Added a "Loop-Stopper" warning when a :rewrite rule is specified with a :loop-stopper field that contains illegal entries that will be ignored. Thanks to Jared Davis for recommending such a warning.

Added a substantial documentation topic that provides a beginner's guide to the use of quantification with defun-sk in ACL2. Thanks to Sandip Ray for contributing this guide, to which we have made only very small modifications. See quantifier-tutorial.

Defun-sk now allows the keyword option :strengthen t, which will generate the extra constraint that that is generated for the corresponding defchoose event; see defchoose. Thanks to Dave Greve for suggesting this feature.

BUG FIXES

Fixed a soundness bug related to the use of mbe inside encapsulate events. An example proof of nil (before the fix) is in a comment in (deflabel note-3-4 ...) in the ACL2 source code. We therefore no longer allow calls of mbe inside encapsulate events that have non-empty signatures.

Fixed a bug related to the definition of a function supporting the macro value-triple. Although this bug was very unlikely to affect any user, it could be carefully exploited to make ACL2 unsound:

(defthm fact
  (equal (caadr (caddr (value-triple-fn '(foo 3) nil nil)))
         'value) ; but it's state-global-let* in the logic
  :rule-classes nil)
(defthm contradiction
  nil
  :hints (("Goal" :use fact :in-theory (disable (value-triple-fn))))
  :rule-classes nil)

Non-LOCAL definitions of functions or macros are no longer considered redundant with built-ins when the built-ins have special raw Lisp code, because ACL2 was unsound without this restriction! A comment about redundant definitions in source function chk-acceptable-defuns shows how one could prove nil without this new restriction. Note that system utility :redef+ removes this restriction.

Although ACL2 already prohibited the use of certain built-in :program mode functions for verify-termination and during macroexpansion, we have computed a much more complete list of functions that need such restrictions, the value of constant *primitive-program-fns-with-raw-code*.

Modified what is printed when a proof fails, to indicate more clearly which event failed.

Fixed a problem with dmr in CCL (OpenMCL) that was causing a raw Lisp break after an interrupt in some cases. Thanks to Gary Byers for a suggestion leading to this fix.

Fixed bugs in proof-checker code for dealing with free variables in hypotheses.

Upon an abort, the printing of pstack and gag-mode summary information for other than GCL was avoided when inside a call of ld. This has been fixed.

(Windows only) Fixed bugs for ACL2 built on SBCL on Windows, including one that prevented include-book parameters :dir :system from working, and one that prevented certain compilation. Thanks to Peter Dillinger for bringing these to our attention and supplying a fix for the second. Thanks also to Andrew Gacek for bringing include-book issues to our attention. Also, fixed writing of file saved_acl2 at build time so that for Windows, Unix-style pathnames are used.

Fixed a hard Lisp error that could occur with keywords as table names, e.g., (table :a :a nil :put). Thanks to Dave Greve for bringing this problem to our attention and providing this example.

Fixed handling of :OR hints so that proof attempts under an :OR hint do not abort (reverting to induction on the original input conjecture) prematurely. Thanks to Robert Krug for pointing out this problem and pointing to a possible initial fix.

(SBCL and CLISP only) It is now possible to read symbols in the "COMMON-LISP" package inside the ACL2 command loop (see lp). This could cause a raw Lisp error in previous versions of ACL2 whose host Common Lisp was SBCL or CLISP. Thanks to Peter Dillinger for bringing this issue to our attention.

Fixed a bug that was preventing certain hints, such as :do-not hints, from being used after the application of an :or hint. Thanks to Robert Krug for bringing this bug to our attention.

(Hons version only) Fixed a bug in the interaction of memoize (hons version only) with event processing, specifically in interaction with failures inside a call of progn or encapsulate. Thanks to Jared Davis for bringing this bug to our attention and sending an example. A simplified example may be found in a comment in source function table-cltl-cmd, source file history-management.lisp; search for ``Version_3.3'' there.

Fixed cw-gstack so that its :evisc-tuple is applied to the top clause, instead of using (4 5 nil nil) in all cases. If no :evisc-tuple is supplied then (term-evisc-tuple t state) is used for the top clause, as it is already used for the rest of the stack.

Fixed a bug in the interaction of proof-trees with :induct hint value :otf-flg-override. Thanks to Peter Dillinger for reporting this bug and sending an example that evokes it.

Fixed bugs in :pr and find-rules-of-rune for the case of rule class :elim. Thanks to Robert Krug and Jared Davis for bringing these related bugs to our attention.

Improved failure messages so that the key checkpoints are printed only once when there is a proof failure. Formerly, a proof failure would cause the key checkpoints to be printed for every encapsulate or certify-book superior to the proof attempt.

Fixed a bug in generation of guards for calls of pkg-witness. Thanks to Mark Reitblatt for sending an example showing this bug. The bug can be in play when you see the message: ``HARD ACL2 ERROR in MAKE-LAMBDA-APPLICATION: Unexpected unbound vars ("")''. A distillation of Mark's example that causes this hard error is as follows.

(defun foo (x)
  (declare (xargs :guard t))
  (let ((y x)) (pkg-witness y)))

The cond macro now accepts test/value pairs of the form (T val) in other than the last position, such as the first such pair in (cond (t 1) (nil 2) (t 3)). Thanks to Jared Davis for sending this example and pointing out that ACL2 was sometimes printing goals that have such a form, and hence cannot be submitted back to ACL2. A few macros corresponding to cond in some books under books/rtl and books/bdd were similarly modified. (A second change will probably not be noticeable, because it doesn't affect the final result: singleton cond clauses now generate a call of or in a single step of macroexpansion, not of if. For example, (cond (a) (b x) (t y)) now expands to (OR A (IF B X Y)) instead of (IF A A (IF B X Y)). See the source code for cond-macro for a comment about this change.)

Fixed a bug in the interaction of proof-checker command DV, including numeric (``diving'') commands, with the add-binop event. Specifically, if you executed (add-binop mac fn) with fn having arity other than 2, a proof-checker command such as 3 or (dv 3) at a call of mac could have the wrong effect. We also fixed a bug in diving with DV into certain AND and OR calls. Thanks for Mark Reitblatt for bringing these problems to our attention with helpful examples.

Fixed a couple of bugs that were causing an error, ``HARD ACL2 ERROR in RENEW-NAME/OVERWRITE''. Thanks to Sol Swords for bringing the first of these bugs to our attention.

Fixed a bug that could cause certify-book to fail in certain cases where there are local make-event forms.

Fixed a bug in start-proof-tree that could cause Lisp to hang or produce an error. Thanks to Carl Eastlund for sending an example to bring this bug to our attention.

Fixed a bug in the proof output, which was failing to report cases where the current goal simplifies to itself or to a set including itself (see specious-simplification).

Fixed a bug in with-prover-time-limit that was causing a raw Lisp error for a bad first argument. Thanks to Peter Dillinger for pointing out this bug.

The following was claimed in :doc note-3-3, but was not fixed until the present release:
Distributed directory doc/HTML/ now again includes installation instructions, in doc/HTML/installation/installation.html.

In certain Common Lisp implementations -- CCL (OpenMCL) and LispWorks, at least -- an interrupt could leave you in a break such that quitting the break would not show the usual summary of key checkpoints. This has been fixed.

NEW AND UPDATED BOOKS

Updated books/clause-processors/SULFA/ with a new version from Erik Reeber; thanks, Erik.

Added new books directory tools/ from Sol Swords. See books/tools/Readme.lsp for a summary of what these books provide.

The distributed book books/misc/file-io.lisp includes a new utility, write-list!, which is like write-list except that it calls open-output-channel! instead of open-output-channel. Thanks to Sandip Ray for requesting this utility and assisting with its implementation.

Added record-update macro supplied by Sandip Ray to distributed book books/misc/records.lisp.

Sandip Ray has contributed books that prove soundness and completeness of different proof strategies used in sequential program verification. Distributed directory books/proofstyles/ has three new directories comprising that contribution: soundness/, completeness/, and counterexamples/. The existing books/proofstyles/ directory has been moved to its subdirectory invclock/.

Jared Davis has contributed a profiling utility for ACL2 built on CCL (OpenMCL). See books/misc/oprof.lisp. Thanks, Jared.

ACL2 utilities getprop and putprop take advantage of under-the-hood Lisp (hashed) property lists. The new book books/misc/getprop.lisp contains an example showing how this works.

Added the following new book directories: books/paco/, which includes a small ACL2-like prover; and books/models/jvm/m5, which contains the definition of one of the more elaborate JVM models, M5, along with other files including JVM program correctness proofs. See files Readme.lsp in these directories, and file README in the latter.

Added books about sorting in books/sorting. See Readme.lsp in that directory for documentation.

Added book books/misc/computed-hint-rewrite.lisp to provide an interface to the rewriter for use in computed hints. Thanks to Jared Davis for requesting this feature.

Jared Davis has provided a pseudorandom number generator, in books/misc/random.lisp.

Robert Krug has contributed a new library, books/arithmetic-4/, for reasoning about arithmetic. He characterizes it as being more powerful than its predecessor, books/arithmetic-3/, and without its predecessor's rewriting loops, but significantly slower than its predecessor on some theorems.

Incorporated changes from Peter Dillinger to verify guards for functions in books/ordinals/lexicographic-ordering.lisp (and one in ordinal-definitions.lisp in that directory).

A new directory, books/hacking/, contains a library for those who wish to use trust tags to modify or extend core ACL2 behavior. Thanks to Peter Dillinger for contributing this library. Obsolete version books/misc/hacker.lisp has been deleted. Workshop contribution books/workshops/2007/dillinger-et-al/code/ is still included with the workshops/ tar file, but should be considered deprecated.

In books/make-event/assert.lisp, changed assert! and assert!-stobj to return (value-triple :success) upon success instead of (value-triple nil), following a suggestion from Jared Davis.

EMACS SUPPORT

Changed emacs/emacs-acl2.el so that the fill column default (for the right margin) is only set (still to 79) in lisp-mode.

Modified Emacs support in file emacs/emacs-acl2.el so that names of events are highlighted just as defun has been highlighted when it is called. Search in the above file for font-lock-add-keywords for instructions on how to eliminate this change.

The name of the temporary file used by some Emacs utilities defined in file emacs/emacs-acl2.el has been changed to have extension .lsp instead of .lisp; thus it is now temp-emacs-file.lsp. Also, `make' commands to `clean' books will delete such files (specifically, books/Makefile-generic has been changed to delete temp-emacs-file.lsp).