|
|
|---|
|
|
|
|---|
ACL2 Version 4.3 (July, 2011) 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
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 andintersection-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 ruleconsp-assoc-equal (formerly two enabled rules,consp-assoc-eq andconsp-assoc ) but adding this theorem as a:forward-chaining rule, and similarly fortrue-list-listp-forward-to-true-listp-assoc-equal (and eliminating ruletrue-list-listp-forward-to-true-listp-assoc-eq ; and disabling ruletrue-listp-cadr-assoc-eq-for-open-channels-p . Also, theoremall-boundp-preserves-assoc has been renamed toall-boundp-preserves-assoc-equal and also strengthened.o Some guards were slightly improved (logically weaker or the same).
Improved
Added the symbols flet and with-local-stobj to
A small change was made to the processing of more than one
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
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
Show-accumulated-persistence may take a new argument,
Improved trace$ so that
The system function
An obscure proof-builder change, unlikely to affect users, replaces
the state global variables
State globals
(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 `
We no longer print induction schemes with gag-mode; use
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 fileld.lisp ).
The undocumented (but sometimes useful) functions
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
NEW FEATURES
New macros mv?-let and mv? extend the functionality 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
New macros,
The proof-builder command
The reports generated by forward-chaining, forward-chaining-reports,
have been changed to indicate when a conclusion reached by forward chaining is
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 !>
Thanks to David Rager for contributing this macro.
The macro defattach may now be supplied the argument
You can now limit the printing of subgoal names when using
A new proof-builder command,
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
Exhaustive matching for the case of free-variables has been extended
to type-prescription rules, in analogy to the default setting
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
(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
It had been possible to prove
(defthm host-lisp-is-ccl (equal (cdr (assoc 'host-lisp *initial-global-table*)) :ccl) :rule-classes nil)
This hole has been plugged by moving the setting of
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
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
(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
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
Terms of the form
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")))
Moreover, the corresponding error message has been fixed. Thanks to Jared Davis and Sandip Ray for relevant discussions.
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
It had been the case that the
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
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
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 (append x y) binary-append
but they did not allow explicit specification of
:pl2 (append x y) (:definition binary-append)
The following example illustrates a bug in the processing of (admittedly
obscure) hints of the form
(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
(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 the ACL2 Books web page. 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, filebooks/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 bookbooks/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
The HTML documentation no longer has extra newlines in <pre> environments.
Statistics on ACL2 code size may be found in distributed file
Fixed the build process to pay attention to environment variable
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
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 returnnil . 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 an 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.