Note-3-4
ACL2 Version 3.4 (August, 2008) 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 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-builder behaves a little differently under gag-mode. Now, proof-builder commands that call the theorem prover to create
new proof-builder goals, such as bash and induct (see proof-builder-commands), will show key checkpoints when in gag-mode.
As before, proof-builder 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-builder 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 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-'' utilities 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 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*. [This constant was renamed
*initial-program-fns-with-raw-code* after Version 8.0.]
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-builder 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-builder 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-builder 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 to 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).
