|
|
|---|
|
|
|
|---|
ACL2 Version 3.3 (November, 2007) 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 `
Made a change to allow
Computed hints (see computed-hints) may now produce a
so-called ``error triple'', i.e., a result of the form
New hints provide additional control of the theorem prover, as follows.
See hints for more details, and see new distributed book directory
o The hint
:OR (hints-1 ... hints-k) causes an attempt to prove the specified goal using eachhints-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 bookbooks/hints/merge.lisp . It is useful for combining hints.o A sophisticated yet useful custom hint is the
:CONSIDER hint implemented in distributed bookbooks/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 bookbooks/hints/consider-hint-tests.lisp for examples.
A new hint,
Enhanced
Added macros
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
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,
Sandip Ray has contributed a book,
Wrote and incorporated new utility for listing all the theorems in an
included book. See
The new distributed book
(Low-level printing improvement) A new function,
The event add-include-book-dir can now take a relative pathname as an argument. Formerly, it required an absolute pathname.
A new book,
ACL2 now provides limited support for the Common Lisp primitive
Added a definition of boole$, a close analogue of Common Lisp
function
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
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-builder commands for the
prover, such as
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
Fixed small proof-builder issues related to packages. Emacs
commands
Fixed a bug that allowed certify-book to succeed without specifying
value
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
Distributed directory
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 andC-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
Fixed a bug that was avoiding compilation of some executable counterparts
(sometimes called ``*1* functions'') during certify-book, and also
during include-book with
Incorporated a fix from Eric Smith for a typo (source function
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
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
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
Made a slight heuristic change, so that when a hypothesis with let
or mv-let subterms (i.e. lambda subterms) rewrites to
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 utilities
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 gag-mode,
set-print-clause-ids,
Output from the proof-builder is now always enabled when invoking verify, even if it is globally inhibited (see set-inhibit-output-lst).
Improved the message printed when an
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
Modified macro
Several improvements have been made to the experimental hons/memoization version of ACL2. See hons-and-memoization.
The distributed books directory,