NOTE-3-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 3.2.1 into new features, bug fixes, prover algorithm enhancements, and miscellaneous. Also see note-3-2-1 for other changes since Version 3.2.

NEW FEATURES

A new ``gag-mode'' provides less verbose, more helpful feedback from the theorem prover, in support of The Method (see the-method). See set-gag-mode. We recommend the use of gag-mode, which may become the default in future ACL2 releases, and we welcome suggestions for improvement. We thank Robert Krug and Sandip Ray for helpful feedback in the design of gag-mode. Note that when proofs fail, then even without gag-mode and even if proof output is inhibited, the summary will contain a useful listing of so-called ``key checkpoints'' (see set-gag-mode).

Added support for a leading `~' in filenames. Thanks to Bob Boyer for suggesting this enhancement. Note that since `~/' depends on the user, it is disallowed in books to be certified (see certify-book), since otherwise an include-book form in a book, b, could have a different meaning at certification time than at the time include-book is later executed on book b.

Made a change to allow (time$ FORM) and (with-prover-time-limit TIME FORM) when FORM includes make-event calls that change the ACL2 world. Thanks to Jared Davis for requesting such support for time$.

Computed hints (see computed-hints) may now produce a so-called ``error triple'', i.e., a result of the form (mv erp val state), where a non-nil erp causes an error, and otherwise val is the value of the hint. It remains legal for a computed hint to return a single ordinary value; indeed, the symbol form of a computed hint must still be a function that returns an ordinary single value.

New hints provide additional control of the theorem prover, as follows. See hints for more details, and see new distributed book directory books/hints/ for examples, in particular file basic-tests.lisp in that directory for simple examples.

o The hint :OR (hints-1 ... hints-k) causes an attempt to prove the specified goal using each hints-i in turn, until the first of these succeeds. If none succeeds, then the prover proceeds after heuristically choosing the ``best'' result, taking into account the goals pushed in each case for proof by induction.

o A custom hint is a keyword that the user associates with a corresponding hint-generating function by invoking add-custom-keyword-hint. Thus, a custom hint may be viewed as a convenient sort of computed hint.

o A custom hint, :MERGE, is implemented in distributed book books/hints/merge.lisp. It is useful for combining hints.

o A sophisticated yet useful custom hint is the :CONSIDER hint implemented in distributed book books/hints/consider-hint.lisp. With this hint, you can for example give the equivalent of a :USE hint without the need to supply an instantiation. Include that book in order to see documentation online with :doc consideration, and see the book books/hints/consider-hint-tests.lisp for examples.

A new hint, :reorder, allows the specification of which subgoals are to be considered first. Thanks to Sandip Ray for putting forward this idea.

Enhanced set-saved-output by supporting a second argument of :same, which avoids changing which output is inhibited.

Added macros thm? and not-thm? to distributed book books/make-event/eval.lisp, so that it's easy to test within a certified book that a proof attempt succeeds or that it fails.

Added printing function cw!, which is analogous to cw just as fmt! is to fmt, i.e., printing so that the result can be read back in. Thanks to Jared Davis for suggesting this enhancement (after doing his own implementation).

The ACL2 customization file can now be specified using environment variable ACL2-CUSTOMIZATION. See acl2-customization. Thanks to Peter Dillinger for requesting this feature.

Added new emacs capabilities for proof trees (all documented in emacs):

o New function start-proof-tree-noninteractive, for example
(start-proof-tree-noninteractive "*shell*")

o C-z o Switch to another frame

o C-z b Switch to prooftree buffer

o C-z B Switch to prooftree buffer in "prooftree-frame" frame

Added Common Lisp function, search, as a macro in logic mode, with limited support for keyword arguments. Thanks to Warren Hunt for requesting this addition.

Sandip Ray has contributed a book, books/make-event/defrefine.lisp, that provides a collection of macros to aid in reasoning about ACL2 functions via refinement.

Wrote and incorporated new utility for listing all the theorems in an included book. See books/misc/book-thms.lisp. Thanks to Jared Davis for requesting this functionality.

The new distributed book misc/defp.lisp generalizes the defpun macro to allow more general forms of tail recursion.

(Low-level printing improvement) A new function, set-ppr-flat-right-margin, allows the right margin for certain kinds of ``flat'' printing to exceed column 40. Thanks to Jared Davis for pointing out that state global variables 'fmt-hard-right-margin and 'fmt-soft-right-margin are not alone sufficient to extend the right margin in all cases.

The event add-include-book-dir can now take a relative pathname as an argument. Formerly, it required an absolute pathname.

A new book, books/misc/defopener.lisp, provides a utility creating a theorem that equates a term with its simplification.

ACL2 now provides limited support for the Common Lisp primitive FLET, which supports local function bindings. See flet. Thanks to Warren Hunt for requesting this feature.

Added a definition of boole$, a close analogue of Common Lisp function boole. Thanks to Bob Boyer for providing an initial implementation.

BUG FIXES

Fixed defstobj to inhibit a potentially useless theory warning.

Fixed a bug in the application of certify-book to relative pathnames for files in other than the current directory. Thanks to Amr Helmy for bringing this bug to our attention.

Fixed a bug in :pl and :pr for displaying rules of class :meta. Thanks to Jared Davis for finding this bug and providing a fix.

Formerly, set-default-backchain-limit was not a legal event form for encapsulate forms and books. This has been fixed. Thanks to Robert Krug and Sandip Ray for bringing this bug to our attention.

Fixed the handling of hints in proof-checker commands for the prover, such as bash -- see proof-checker-commands -- so that the user can override the default settings of hints, in particular of :do-not and :do-not-induct hints attached to "Goal". This fix also applies to the distributed book misc/bash.lisp, where Robert Krug noticed that he got an error with :hints (("Goal" :do-not '(preprocess))); we thank Robert for pointing out this problem.

Fixed a bug in handling of stobjs occurring in guards of functions whose guards have been verified. In such cases, a raw Lisp error was possible when proving theorems about non-''live'' stobjs. We thank Daron Vroon for sending us an example that highlighted this bug. The following (simpler) example causes such an error in previous versions of ACL2.

(defstobj st fld)
(defun foo (st)
  (declare (xargs :stobjs st :guard (fld st)))
  st)
(thm (equal (foo '(3))
            '(3)))

The dmr feature for dynamic monitoring of rewrites had a bug, where the file used for communicating with emacs was the same for all users, based on who built the ACL2 executable image. This has been fixed. Thanks to Robert Krug for bringing this bug to our attention.

Fixed a bug in some warnings, in particular the warning for including an uncertified book, that was giving an incorrect warning summary string.

Inclusion of uncertified books erroneously re-used make-event expansions that were stored in stale certificates. This is no longer the case. Thanks to Jared Davis for bringing this bug to our attention.

Fixed a bug that was disallowing calls of with-output in events that were executing before calling certify-book.

Modified the functionality of binop-table so other than binary function symbols are properly supported (hence with no action based on right-associated arguments). See add-binop.

Fixed small proof-checker issues related to packages. Emacs commands ctrl-t d and ctrl-t ctrl-d now work properly with colon (`:') and certain other punctuation characters. The p-top command now prints ``***'' regardless of the current package.

Fixed a bug that allowed certify-book to succeed without specifying value t for keyword argument :skip-proofs-okp, even with include-book events in the certification world depending on events executed under skip-proofs.

Improved show-accumulated-persistence in the following two ways. Thanks to Robert Krug and Bill Young for requesting these improvements and for providing useful feedback.

o It can provide more complete information when aborting a proof.

o The :frames reported for a rule are categorized as ``useful'' and ``useless'' according to whether they support ``useful'' or ``useless'' :tries of that rule, respectively. See accumulated-persistence for further explanation.

Modified make-event so that the reported time and warnings include those from the expansion phase. In analogy with encapsulate and progn, the rules reported still do not include those from subsidiary events (including the expansion phase). A related change to ld avoids resetting summary information (time, warnings) with each top-level form evaluation; events already handle this information themselves.

Fixed set-inhibit-output-lst so that all warnings are inhibited when warning! but not warning is included in the list. Formerly, only soundness-related warnings were inhibited in this case. Thanks to Eric Smith for bringing this bug to our attention.

Distributed directory doc/HTML/ now again includes installation instructions (which was missing in Version_3.2.1), in doc/HTML/installation/installation.html.

Some fixes have been made for proof-tree support.

o Proof-tree output is no longer inhibited automatically during certify-book, though it continues to be inhibited by default (i.e., ACL2 continues to start up as though set-inhibit-output-lst has been called with argument '(proof-tree)).

o Fixed a bug in Xemacs support for proof-tree help keys C-z h and C-z ?.

o Fixed a bug in proof-trees that was failing to deal with the case that a goal pushed for proof by induction is subsumed by such a goal to be proved later. Now, the proof-tree display regards such subsumed goals as proved, as is reported in the theorem prover's output.

Fixed a bug that was disallowing value-triple forms inside encapsulate forms in a certification world (see portcullis).

If the :load-compiled-file argument of a call of include-book is :comp, then an existing compiled file will be loaded, provided it is more recent than the corresponding book (i.e., .lisp file). A bug was causing the compiled file to be deleted and then reconstructed in the case of :comp, where this behavior was intended only for :comp!.

Fixed a bug that was avoiding compilation of some executable counterparts (sometimes called ``*1* functions'') during certify-book, and also during include-book with :load-compiled-file value of :comp or :comp!). Thanks to Eric Smith for sending a small example to bring this bug to our attention.

Incorporated a fix from Eric Smith for a typo (source function ancestors-check1) that could cause hard Lisp errors. Thanks, Eric!

Fixed the following issues with packages and book certificates. See hidden-death-package if you are generally interested in such issues, and for associated examples, see comments on ``Fixed the following issues with packages'' in note-3-3 in the ACL2 source code.

o Reduced the size of .cert files by eliminating some unnecessary defpkg events generated for the portcullis.

o Fixed a bug that has caused errors when reading symbols from a portcullis that are in undefined packages defined in locally included books.

o Fixed a bug that could lead to failure of include-book caused by a subtle interaction between set-ignore-ok and defpkg events generated for the portcullis of a certificate.

PROVER ALGORITHM ENHANCEMENTS

Non-linear arithmetic (see non-linear-arithmetic) has been improved to be more efficient or more powerful in some cases. Thanks to Robert Krug for contributing these improvements.

Improved certain (so-called ``type-set'') reasoning about whether or not expressions denote integers. Thanks to Robert Krug for contributing code to implement this change, along with examples illustrating its power that are now distributed in the book books/misc/integer-type-set-test.lisp.

Improved ACL2's heuristics for relieving hypotheses, primarily to use linear reasoning on conjuncts and disjuncts of the test of an if expression. For example, given a hypothesis of the form (if (or term1 term2) ...), ACL2 will now use linear reasoning to attempt to prove both term1 and term2, not merely for term2. Thanks to Robert Krug for supplying examples illustrating the desirability of such an improvement and for useful discussions about the fix.

Made a slight heuristic change, so that when a hypothesis with let or mv-let subterms (i.e. lambda subterms) rewrites to t, then that hypothesis is necessarily eliminated. Thanks to Jared Davis for sending an example that led us to develop this change, and thanks to Robert Krug for a helpful discussion.

MISCELLANEOUS

Added documentation on how to use make-event to avoid duplicating expensive computations, thanks to Jared Davis. See using-tables-efficiently.

Modified the error message for calls of undefined functions to show the arguments. Thanks to Bob Boyer for requesting this enhancement.

Modified utilies :pr, :pr!, :pl, and :show-bodies to incorporate code contributed by Jared Davis. That code defines low-level source functions info-for-xxx that collect information about rules, which is thus available to advanced users.

Dynamic monitoring of rewrites (see dmr) has been improved in the following ways, as suggested by Robert Krug.

o Some stale entries from the rewrite stack are no longer printed, in particular above ADD-POLYNOMIAL-INEQUALITIES.

o An additional rewrite stack entry is made when entering non-linear arithmetic (see non-linear-arithmetic).

o An ADD-POLYNOMIAL-INEQUALITIES entry is printed with a counter, to show how often this process is called.

Modified save-exec so that the newly-saved image will have the same raw Lisp package as the existing saved image. This is a very technical change that will likely not impact most users; for example, the package in the ACL2 read-eval-print loop (see lp) had already persisted from the original to newly-saved image. Thanks to Jared Davis for suggesting this change.

Changed make-event expansion so that changes to set-saved-output, set-print-clause-ids, set-fmt-soft-right-margin, and set-fmt-hard-right-margin will persist after being evaluated during make-event expansion. (Specifically, *protected-system-state-globals* has been modified; see make-event-details.) Thanks to Jared Davis for bringing this issue to our attention.

Output from the proof-checker is now always enabled when invoking verify, even if it is globally inhibited (see set-inhibit-output-lst).

Improved the message printed when an :induct hint fails, to give more information in some cases. Thanks to Rex Page for suggesting where an improvement could be made and providing useful feedback on an initial improvement.

Added a warning for congruence rules (see defcong) that specify iff as the second equivalence relation when equal can be used instead. Those who heed these warnings can eliminate certain subsequent double-rewrite warnings for rewrite rules with conclusions of the form (iff term1 term2), and hence implicitly for Boolean conclusions term1 that are interpreted as (iff term1 t). Thanks to Sarah Weissman for sending us an example that highlighted the need for such a warning.

Modified macro :redef! (which is for system implementors) so that it eliminates untouchables.

Several improvements have been made to the experimental hons/memoization version of ACL2. See hons-and-memoization.

The distributed books directory, (@ distributed-books-dir), is now printed in the start-up message.