defattach.
CHANGES TO EXISTING FEATURES
There have been extensive changes to the handling of compiled files for books, which may generally be invisible to most users. The basic idea is that when compiled files are loaded on behalf of
include-book, they are
now loaded before events in the book are processed, not afterwards. This can
speed up calls of include-book, especially if the underlying Lisp
compiles all definitions on the fly (as is the case for CCL and SBCL). One
functional change is that for keyword argument :load-compiled-file of
include-book, the values :comp-raw, :try, and :comp! are no
longer legal. (Note that the handling of :comp-raw was actually broken,
so it seems that this value wasn't actually used by anyone; also, the
handling of :comp! formerly could cause an error in some Lisp platforms,
including SBCL.) Another change is that if include-book is called with
:load-compiled-file t, then each sub-book must have a compiled file or a
so-called ``expansion file''; see book-compiled-file. In the unlikely event
that this presents a problem, the makefile provides a way to build with
compilation disabled; see compilation. Users of raw mode
(see set-raw-mode) will be happy to know that include-book now works
if there an up-to-date compiled file for the book, since portcullis
commands are now incorporated into that compiled file. The mechanism for
saving expansion files has changed, and the :save-expansion argument of
certify-book has been eliminated; see certify-book. More discussion
of ACL2's new handling of book compilation is described in a new
documentation topic; see book-compiled-file.It was possible to get a hard Lisp error when certifying a book with a redundant
defconst form whose term is not identical to the existing
defconst form for the same name. The following example illustrates the
problem, which has been fixed (as part of the change in handling of compiled
files for books, described above). Imagine that after the initial
(in-package "ACL2") form, file foo.lisp has just the form
(defconst *a* (append nil nil)). Then before the fix, we could have:
ACL2 !>(defconst *a* nil) [[output omitted]] ACL2 !>(certify-book "foo" 1) [[initial output omitted] * Step 5: Compile the functions defined in "/v/joe/foo.lisp". Compiling /v/joe/foo.lisp. End of Pass 1. End of Pass 2. OPTIMIZE levels: Safety=0 (No runtime error checking), Space=0, Speed=3 Finished compiling /vjoe/foo.lisp. Loading /v/joe/foo.lispError: Illegal attempt to redeclare the constant *A*.
The wormhole facility has been changed to repair a bug that allowed
guard violations to go undetected. The major change has to do with the
treatment of what used to be called the ``pseudo-flag'' argument which has
been replaced by a quoted lambda expression. See note-4-0-wormhole-changes
for help in converting calls of wormhole. Also see see wormhole and
see wormhole-eval.
The function assign-wormhole-output has been eliminated but its
functionality can be provided by wormhole-eval.
The ACL2 tutorial has been greatly expanded, for example to include a
self-contained discussion of rewriting. See acl2-tutorial.
mbe macro and must-be-equal function were
disallowed in any definition within an encapsulate having a non-empty
signature. Now, these are allowed provided the definition has been declared
to be non-executable (see defun-nx). As a result, defevaluator
events may now include must-be-equal among the function symbols
known by the evaluator; this had not previously been allowed. Thanks to Sol
Swords for discussions leading to this relaxation for defevaluator.
Princ$ now prints strings more efficiently. Thanks to Jared Davis for
suggesting the improvements to princ$.
The use of
xargs declaration :non-executable t no longer requires
the absence of state or declared stobjs among the formal
parameters of a function definition. As before, the use of
:non-executable t turns off single-threadedness checking for the body,
and also as before, attempts to execute the function will fail. Thanks to
Sol Swords for requesting this relaxation (for automatic generation of
so-called ``flag functions'' for definitions using mutual-recursion).nonlinearp-default-hint in distributed book
books/hints/basic-tests.lisp. Thanks to Robert Krug for useful
discussions, in particular suggesting the above example as one to be
explained with the documentation.time$ macro has been enhanced to allow user control of the timing
message that is printed, and of when it is printed. See time$. Thanks to
Jared Davis for providing the essential design, helpful documentation
(largely incorporated), and an initial implementation for raw Lisp.:ttags argument to include-book had been required when
including a certified book that uses trust tags. This is no longer the case:
essentially, :ttags defaults to :all except that warnings will be
printed. Thanks to Jared Davis for requesting such a relaxation, and to him
and Sandip Ray for useful discussions.mv-let has been modified so that the single-step
macroexpansion (see trans1) of its calls can be evaluated. Thanks to Pete
Manolios for bringing this evaluation issue to our attention and ensuing
discussions. On a related note, all calls of so-called ``guard-holders''
-- prog2$, must-be-equal (from calls of see mbe),
ec-call, and mv-list -- are now removed before storing
hypotheses of rules of class :rewrite, :definition, or
:linear.
The handling of fmt directive ~s has been modified so that if the
argument is a symbol that would normally be printed using vertical bars
(|), then that symbol is printed as with ~f. Thanks to Jared Davis
for providing the following example showing that treatment of ~s was a
bit unexpected: (cw "~s0.~%" '|fo\|o|).
Error messages have been improved for ill-formed terms (in ACL2's so-called ``translation'' routines). Thanks to Jared Davis for requesting such an enhancement.
Modified defun-sk so that it executes in :logic mode.
Previously, evaluation of a defun-sk event in :program mode
caused a somewhat inscrutable error, but now, :program mode is
treated the same as :logic mode for purposes of defun-sk.
The ``system hacker'' commands
(redef+) and
(redef-) are now embedded event forms
(see embedded-event-form), hence may be used in books as well as in
progn and encapsulate events. Also, these two commands are
now no-ops in raw Lisp.worldp (in the "ACL2" package) has been renamed
to plist-worldp.
The function gc$-fn (resulting from macroexpansion of gc$) is now
in :logic mode. Thanks to Jared Davis for requesting this change.
The user now has control over whether compilation is used, for example
whether or not
certify-book compiles by default, using function
set-compiler-enabled. See compilation.
The "Ttags" warning that can be printed by include-book is now
given even if set-inhibit-output-lst has specified warning. To
suppress it, specify warning! instead, for example,
(set-inhibit-output-lst '(acl2::warning! acl2::proof-tree)).
On occasion, ACL2 prints the message ``Flushing current installed world'' as
it cleans up when certain actions (installing a world) are interrupted.
This operation has been sped up considerably. If your session includes many
events, you can probably speed up any such operation further by invoking
reset-prehistory. Thanks to Jared Davis for sending a query that led
us to make this improvement.
Calls of the form (ec-call (must-be-equal logic exec)) are no longer
allowed, since we do not have confidence that they would be handled
correctly.
The underlying function for good-bye (and hence for exit and
quit) is now in :logic mode. Thanks to Jared Davis for
requesting this enhancement.
We now require that every function symbol in the signature of an
encapsulate event have a :logic mode definition at the end of
the first pass, not merely a :program mode definition (which
formerly was sufficient). You can still define such a function in
:program mode, provided it is followed by a :logic mode definition
(where of course both definitions are local, since we are discussing
functions is introduced in the signature). Thanks to Carl Eastlund for
bringing this issue to our attention. (Note: An analogous modification has
been made for :bdd hints as well.)
The following functions now have raw Lisp implementations that may run faster
than their ACL2 definitions: assoc-eq, assoc-equal,
member-eq, member-equal, subsetp-eq, subsetp-equal,
remove-eq, remove-equal, position-eq, and
position-equal. Thanks to Jared Davis for suggesting that we consider
such an improvement.
We now avoid infinite loops caused when tracing functions that implement
trace$. Thanks to Rob Sumners and Eric Smith for useful discussions.
The implementation of trace! has been modified slightly, to accommodate
the fix for ``some holes in the handling of trust tags'' described later,
below.
This item applies unless the host Lisp is GCL. An interrupt (control-c) will
now cause a proof to exit normally in most cases, by simulating a timeout, as
though
with-prover-time-limit had been called with a time-limit of 0.
If the first interrupt doesn't terminate the proof, a second one should do so
(because a different, more ``severe'' mechanism is used after the first
attempt). As a result, redo-flat should work as one might expect even
if a proof is interrupted. Thanks to Dave Greve for requesting this
enhancement to redo-flat.mv-list is the identity function logically, but converts
multiple values to lists. The first argument is the number of values, so an
example form is as follows, where foo returns three values:
(mv-list 3 (foo x y)). Thanks to Sol Swords for requesting this
feature and for reporting a soundness bug in one of our preliminary
implementations.state global variable, host-lisp, has as its value a keyword
whose value depends on the underlying Common Lisp implementation. Use
(@ host-lisp) to see its value.acl2::write-html-file at the end of file
doc/write-acl2-html.lisp. When there are such errors, they should be
easier to understand than previously. Thanks to Alan Dunn for providing the
initial modifications.
It is now possible to inhibit specified parts of the Summary printed at the
conclusion of an event. See set-inhibited-summary-types. Also
see with-output, in particular the discussion of the new
:summary
keyword. Thanks to Sol Swords for requesting more control over the Summary.:hints keyword, :case-split-limitations, can override the
default case-split-limitations settings (see set-case-split-limitations) in
the simplifier. Thanks to Ian Johnson for requesting this addition and
providing an initial implementation.
A new command,
:pl2, allows you to restrict the rewrite rules
printed that apply to a given term. See pl2. Thanks to Robert Krug for
requesting such a capability.IF by non-recursive
functions. Most users need not be concerned with this change, but two proofs
in the regression suite (out of thousands) needed trivial adjustment, so user
proofs could need tweaking. In one application, this modification sped up
proofs by 15%; but the change in runtime for the regression suite is
negligible, so such speedups may vary. Thanks to Sol Swords for providing a
test from ACL2 runs at Centaur Technology, which was useful in re-tuning this
heuristic.case statement. This inefficiency has been removed with a change
that eliminates a hypothesis of the form (not (eql term constant)) when
there is already a stronger hypothesis, equating the same term with a
different constant. Thanks to Sol Swords for bringing this problem to our
attention and suggesting an alternate approach to solving it, which we may
consider in the future if related efficiency problems persist.prog2$ or ec-call, and the first
argument contains no recursive call. These cases are treated more directly
as though the ruler-extender call is replaced by the unique (in the case of
prog2$ and ec-call, the second) argument.
A new :type-prescription rule, true-listp-append, has been
added:
(implies (true-listp b)
(true-listp (append a b)))
If you are interested in the motivation for adding this rule, see comments in
true-listp-append in ACL2 source file axioms.lisp.
The use of
:forward-chaining lemmas has been improved slightly. In
previous versions, a conclusion derived by forward chaining was discarded if
it was derivable by type-set reasoning, since it was ``already provable.''
But this heuristic prevented the conclusion from triggering further forward
chaining. This has been fixed. Thanks to Dave Greve for pointing out this
problem.IF expression into a set of clauses
has been optimized to better handle tests of the form (equal x 'constant)
and their negations. This eliminates an exponential explosion in large case
analyses. But it comes at the inconveience of sometimes reordering the
clauses produced. The latter aspect of this change may require you to change
some Subgoal numbers in proof hints. We apologize for the inconvenience.make-event, when there is
significant sharing of substructure, because of a custom optimization of the
Lisp reader. Thanks to Sol Swords for bringing this efficiency issue to our
attention.make-event evaluation due
to a potentially expensive ``bad lisp object'' check on the expansion
produced by the make-event. This check has been eliminated except in the
case that the expansion introduces packages (for example, by including a book
during the expansion phase that introduces packages). Thanks to Jared for
providing a helpful example.
The application of rules of class :induction had the potential to
loop (as commented in ACL2 source function apply-induction-rule). This
has been fixed. Thanks to Daron Vroon and Pete Manolios for sending nice
examples causing the loop.
Heuristics have been tweaked so that false goals may be simplified to
nil
that had formerly been left unchanged by simplification, perhaps resulting in
useless and distracting proofs by induction. Thanks to Pete Manolios for
pointing out this issue by sending the following example:
(thm (<= (+ 1 (acl2-count x)) 0)). (Technical explanation: When every
literal in a clause simplifications to nil, even though we might not
normally delete one or more such literals, we will replace the entire clause
by the false clause.)take. Thanks to Bob
Boyer for suggesting this improvement.
BUG FIXES
apply-instantiated-elim-rule and
eliminate-destructors-clause1, and comments in the former contain Eric's
example.)nil by exploiting the fact that
portcullis commands were not included in check-sum computations in
a book's certificate. For such a proof of nil, see the relevant
comment in the ACL2 source file ld.lisp under
(deflabel note-4-0 ...).add-include-book-dir. The previous
implementation could allow relative pathnames to be stored in the
portcullis commands of certificates of books, which
perhaps could lead to unsoundness (though we did not try to exploit this to
prove nil). Thanks to Jared Davis for reporting a bug in our first new
implementation. An additional change to both add-include-book-dir and
delete-include-book-dir is that these now work in raw-mode
(see set-raw-mode). Note that it is no longer permitted to make a direct
call of the form (table acl2-defaults-table :include-book-dir-alist ...);
use add-include-book-dir instead.xargs keyword :non-executable.
New macros, defun-nx and defund-nx, have been provided for declaring
functions to be non-executable; see defun-nx. While we expect this bug to
occur only rarely if at all in practice, the following example shows how it
could be evoked.
;;;;;;;;;;;;;;;;;;;;
;;; Book sub.lisp
;;;;;;;;;;;;;;;;;;;;
(in-package "ACL2")
(defun f ()
(declare (xargs :guard t
:non-executable t))
(mv-let (a b c)
(mv 3 4)
(declare (ignore a b))
c))
(defun g ()
(declare (xargs :guard t))
(prog2$ (mv-let (x y z)
(mv 2 3 4)
(declare (ignore x y z))
nil)
(f)))
(defthm g-nil
(equal (g) nil)
:hints (("Goal" :in-theory (disable (f))))
:rule-classes nil)
;;;;;;;;;;;;;;;;;;;;
;;; Book top.lisp
;;;;;;;;;;;;;;;;;;;;
(in-package "ACL2")
(include-book "sub")
(defthm contradiction
nil
:hints (("Goal" :use g-nil))
:rule-classes nil)
defun-nx also prevents
execution of non-executable functions that have been traced. The
following example illustrates the problem; now, the following defun of
g is illegal, and the problem disappears if defun-nx is used
instead.
(defun g (x) ; Use defun-nx to avoid an error after Version_3.6.1.
(declare (xargs :guard t :non-executable t))
x)
(g 3) ; causes error, as expected
(trace$ g)
(g 3) ; returned 3 before the bug fix; after fix, causes error as expected
(make-event '(local ...)). This has
been fixed. Thanks to Sol Swords for bringing this issue to our attention.
Fixed a bug in the heuristic improvement described for Version_3.6 (see note-3-6) as ``We simplified induction schemes....'' The bug had prevented, in unusual cases such as the following (notice the impossible case), a proof by induction.
(defun foo (a x)
(and (consp x)
(case a
(0 (foo (car x) (cdr x)))
(1 (foo (cdr x) (car x)))
(0 (foo a (cons x x))))))
(in-theory (disable (:type-prescription foo)))
(thm (atom (foo a x)))
Macro cw-gstack did not work with an :evisc-tuple argument. This
has been fixed by changing cw-gstack so that it now evaluates its
arguments. Thanks to Sol Swords for bringing this bug to our attention.
Fixed a bug in :pso during the printing of failure messages for
termination proofs.
Fixed a bug in the handling of #. (see sharp-dot-reader). Thanks to Bob
Boyer for bringing this bug to our attention.
Replaced a hard Lisp error with a clean error, in certain cases that a
:hints value is erroneously supplied as a non-nil atom.
Example: (thm (equal x x) :hints 3).
Fixed a bug in the interaction of function tracing with conversion of a
function from :program to :logic mode. The following
example illustrates what had been wrong.
(defun f (x)
(declare (xargs :mode :program))
(car x))
(f 3) ; raw Lisp hard error
(trace$ f)
(f 3) ; raw Lisp hard error (still)
(defun f (x) (car x)) ; upgrade f to :logic mode
(f 3) ; clean guard violation; f is no longer traced
(trace$) ; uh oh - f is shown as traced
(untrace$ f)
(f 3) ; OUCH: hard Lisp error because old :program mode definition of
; the executable counterpart (sometimes called *1*f) was restored!
Made a fix so that when building ACL2 with make option ACL2_SAFETY=3,
there will no longer be any safety-0 compiled code generated. Thanks to Gary
Byers for bringing this bug to our attention.
Fixed a bug in the handling of override-hints that generate custom
keyword hints (see custom-keyword-hints) involving the variable
stable-under-simplificationp. Thanks to Ian Johnson for bringing this
bug to our attention with explanation that included a helpful example,
included as comment in the ACL2 source code for function
apply-override-hint.
The saved_acl2 script in CLISP could contain unexpected characters where
simple newlines were expected. Dave Greve found this in a Cygwin environment
on Windows. Thanks to Dave for reporting this bug and experimenting with a
fix, and thanks to the CLISP folks for providing helpful information.
Fixed a bug that could make :oops cause an error. Also, the
oops command can no longer take you back before a
reset-prehistory event.
(GCL only) Fixed a bug that could occur when calling trace in raw Lisp in
GCL.
Proof summaries have been improved, so that they account for runes used in rewriting that takes place when generating goals to be proved in a forcing round. Thanks to Jared Davis for sending us an example illustrating this issue.
Fixed a bug that (at least in CCL) could put extra backslashes (`\') in
a pathname that ACL2 writes out to the executable script created by a build.
Thanks to Gary Byers for explaining that the CCL behavior is legal (for our
previous use of Common Lisp function merge-pathnames).
We closed some holes in the handling of trust tags (also known as ``ttags'';
see defttag) by
include-book. The following example illustrates this
rather subtle situation. Consider the following book.
(in-package "ACL2")
(make-event
(er-progn
(encapsulate
()
(defttag :foo)
(value-triple "Imagine something bad here!"))
(value '(value-triple :some-value)))
:check-expansion t)
Formerly, the following commands succeeded.
(certify-book "test3" 0 t :ttags :all)
:u
(include-book "test3" :ttags nil)
But because of make-event keyword argument :check-expansion t, we
know that the event (defttag :foo) is evaluated by the above
include-book form, and hence the :ttags argument of
include-book, above, should have specified :foo. The problem was
that defttag forms evaluated during make-event expansion did not
contribute to the trust tag information stored in the book's
certificate. Note: Because of this change, one should avoid using
make-event with :check-expansion t when the expansion would
introduce a defttag event during include-book but not
certify-book time. For an example illustrating this issue,
see make-event-details, specifically the new version of the section labeled
``A note on ttags'' at the end of that documentation topic.
The following example was formerly allowed, but resulted in a guard-verified
function (here, g) whose guard proof obligation is not a theorem outside
the encapsulate event. We now disallow guard verification for
functions introduced inside an encapsulate event unless we determine
that the proof obligations hold outside the encapsulate event as well.
(encapsulate ((f (x) t)) (local (defun f (x) (declare (xargs :guard t)) (consp x))) (defun g (x) (declare (xargs :guard (f x))) (car x)))
NEW AND UPDATED BOOKS AND RELATED INFRASTRUCTURE
We note in particular the new
system/ directory, which begins to specify
ACL2 system code. Some system functions were changed slightly (but with the
expectation of not generally affecting ACL2 behavior) in support of the
development of this directory.make-level paralellism. For example, we have
obtained close to a 12x reduction in time by using
`make -j 24 regression-fast' on a 24-processor machine.
For more information see
books/make-targets, or to include the books/workshops in the
regression run, see books/regression-targets. Thanks to Sol Swords for
providing these nice utilities.GNUmakefile, has been fixed so that the build
processes (which are inherently sequential) will ignore the -j option of
make. Note that regressions can still, however, be done in parallel, as
the -j option will be passed automatically to the appropriate make
command.
EMACS SUPPORT
EXPERIMENTAL VERSIONS
:FORGET is now supported when calling
memoize from within the ACL2 loop, and system function worse-than
is memoized with the :condition that both terms are function
applications (clearing the memo-table after each prover invocation). Thanks
to Jared Davis and Sol Swords for investigating the memoization of
worse-than, and with suitable condition.
David Rager contributed modifications to the parallel version (see parallelism) to take advantage of atomic increments available at least since Version 1.0.21 of SBCL and Version 1.3 of CCL.
Some Related Topics
NOTE-4-0-WORMHOLE-CHANGES -- how to convert calls of wormhole for Version 4.0
