ACL2 Version 4.0 (July, 2010) Notes
NOTE! New users can ignore these release notes, because the documentation has been updated to reflect all changes that are recorded
Below we roughly organize the changes since Version 3.6.1 into the
following categories of changes: existing features, new features, heuristic
improvements, bug fixes, 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. Also see note-3-6-1 for other changes since Version 3.6.
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)
ACL2 !>(certify-book "foo" 1)
[[initial output omitted]
* Step 5: Compile the functions defined in "/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.
Error: 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.
Formerly, the 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).
The documentation has been improved for explaining to advanced users
the details of the ACL2 hint mechanism; see hints-and-the-waterfall,
and see the example about 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.
The 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.
The :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.
The definition of 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
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 or :linear. Thanks to Sol Swords for
requesting this enhancement and sending the following example in the case of
(prog2$ (cw "asdf")
(and (equal (car (cons x y)) x)
(equal (cdr (cons x y)) y))))
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
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
The function symbol 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
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.
Modified the conversion of relative to absolute pathnames in portcullis commands for book certification. Now, more pathnames
remain as relative pathnames.
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
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
The implementation of trace! has been modified slightly, to
accommodate the fix for ``some holes in the handling of trust tags'' described
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. Technical note: for reasons related to
this change, time-limits are no longer checked in evaluator functions
(ev-fncall, ev, ev-lst, ev-fncall-w, ev-w, and
It is now legal for proof-builder macro-commands to appear in
:instructions that are used in place of :hints.
Thanks to Sandip Ray for (most recently) requesting this feature.
The value of :command-conventions for ld special variable
ld-post-eval-print is now treated as though it were t if the value
ld special variable ld-error-triples is nil. The following
example illustrates this change.
ACL2 !>(ld-post-eval-print state) ; default
ACL2 !>(ld-error-triples state) ; default
ACL2 !>(set-ld-error-triples nil state)
*** Then, before the change:
ACL2 !>(mv t 3 state)
*** Instead, after the change:
ACL2 !>(mv t 3 state)
(T 3 <state>)
The default behavior of ld has been changed. Formerly when an
error occurred that halted a subsidiary call of ld, then the parent
ld would continue. That is no longer the case. Consider the following
(ld '((ld '((defun f (x) x)
(defun bad (x)) ; ERROR -- missing the body
(defun g (x) x)))
Formerly, g would be defined in the resulting logical world.
Now, the error halts not only the inner ld but also the outer ld.
See ld, and for details of the new default value for
:ld-error-action, :RETURN!, see ld-error-action. Also see
the paragraph below about a new utility, :p!. Thanks to Robert
Krug and Sandip Ray for helpful discussions.
Environment variable ACL2-CUSTOMIZATION has been replaced by
ACL2_CUSTOMIZATION — that is, the hyphen has been replaced by an
underscore — so that it can be set conveniently in the bash shell.
The ``Warnings:'' summary is now omitted when there are no warnings,
where formerly ``Warnings: None'' was printed. Thanks to Jared Davis for
suggesting this change.
We have modified the generation of constraints for encapsulate
events in two primary ways, neither of them likely to affect many
users. One change is that the virtual movement of definitions and theorems to
in front of an encapsulate event, or of definitions to behind that
event, is no longer inhibited in the case of nested encapsulates with
non-empty signatures. The following example illustrates the other
change, as discussed below.
((f (x) t))
(local (defun f (x) x))
(defun g (x) (cons x (f x)))
(defun h (x) (g x))
(defthm h-is-f (equal (car (h x)) x)))
Previously, the constraint on f and h was essentially the
conjunction of the definition of h and the theorem h-is-f. Now, the
definition of g is conjoined as well; moreover, g receives the same
constraint as do f and h, where previously g was only
constrained by its definition. While we are not aware of a soundness bug
caused by the previous approach, the new approach follows more precisely the
intended notion of constraint.
The use of trace$ (or trace!) option :multiplicity had
been required when option :native was supplied. This is no longer the
case. Also, a bug has been fixed that had prevented :multiplicity from
working properly in GCL and Allegro CL.
Several errors have been eliminated that formerly occurred when the
constraints for a function symbol were unknown because it was constrained
using a dependent clause-processor (see define-trusted-clause-processor. Now, it is assumed that the supporters
argument in a define-trusted-clause-processor event is such that every
ancestor of any function symbol constrained by the ``promised encapsulate'' of
that event among, or ancestral in, those supporters. Thanks to Sol
Swords, Sandip Ray, and Jared Davis for helpful discussions.
The notion of constraint for functions introduced by defun
has been modified slightly. No longer do we remove from the body of the
definition calls of so-called ``guard-holders'': prog2$, must-be-equal, ec-call, and mv-list, and uses of the-error
generated by the. Also, we now expand calls of the-error with
the same aggressive heuristics applied to a number of other functions
(technically, adding it to the list
A new event, defattach, allows evaluation of calls of constrained
(encapsulated) functions. In particular, users can now, in principle,
soundly modify ACL2 source code; please feel free to contact the ACL2
implementors if you are interested in doing so. See defattach.
Eric Smith has noticed that if you exit the break-rewrite loop using
:a! during an ld of a file, then all changes to the
logical world are discarded that were made during that call of ld. A new utility, :p!, pops just one level instead, and avoids
discarding that work. (This change is related to an item above, ``The default
behavior of ld has been changed.'') Thanks to Eric for pointing out
New function 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
A new 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.
It is now possible to write documentation for HTML without error
when there are links to nonexistent documentation topics. See the comments in
macro 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
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
A new :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.
It is now possible to defer and avoid some ttag-related output; see set-deferred-ttag-notes. Thanks to Jared Davis for requesting less verbosity
from ttag-related output.
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.
ACL2 now provides a utility for canonicalizing filenames, so that soft
links are resolved; see canonical-pathname. Moreover, ACL2 uses this
utility in its own sources, which can eliminate some issues. In particular,
include-book with argument :ttags :all no longer breaks when
given a book-name differing from the book-name that was used at certification
time; thanks to Sol Swords for reporting that problem. Also, certain errors
have been eliminated involving the combination of packages in the
certification world and trust tags; thanks to Jared Davis for sending an
example of that problem.
You can now suppress or enable guard-checking for an individual form; see
with-guard-checking. Thanks to Sol Swords for requesting this
The walkabout utility has been documented (thanks to Rob Sumners
for suggesting this documentation). This utility can make it easy to explore
a large cons tree. New interactive commands (pp n) and (pp
print-level print-length) have been added to restrict how much of the
current object is displayed. See walkabout.
Rules of class :type-prescription may now be provided a
:backchain-limit-lst keyword. The default behavior is unchanged, but now
type-set is sensitive not only to the new :backchain-limit-lst of
a :type-prescription rule (if supplied) but to the default-backchain-limit of the current logical world. Setting of
backchain-limits can now specify either the new (type-set) limit or the old
limit (for rewriting); see set-default-backchain-limit and see set-backchain-limit. Moreover, the functions default-backchain-limit
and backchain-limit now take a second argument of :ts or
:rewrite to specify which backchain-limit is desired.
The so-called ``too-many-ifs'' heuristic has been modified. Such a
heuristic has been employed in ACL2 (and previous Boyer-Moore provers) for
many years, in order to limit the introduction of calls of 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.
Guard proof obligations could have size quadratic in the number of clauses
in a 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.
We adjusted the heuristics for determining induction schemes in the
presence of ruler-extenders, when handling calls of a function symbol
that is a ruler-extender, in either of two cases: either the function takes
only one argument; or the function is 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
(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
The fundamental utility that turns an 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 inconvenience 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
Certification can now run faster (specifically, the compilation phase) for
books with very large structures generated by 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
Jared Davis reported inefficiency in certain 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 simplifies to nil, even though we might not normally delete one
or more such literals, we will replace the entire clause by the false
Improved the efficiency of the built-in function, take. Thanks to
Bob Boyer for suggesting this improvement.
ACL2 can now use evaluation to relieve hypotheses when applying
:type-prescription rules. Thanks to Peter Dillinger and Dave
Greve for requesting this enhancement, and to Robert Krug for a relevant
discussion long ago.
Evaluation has been sped up during theorems for calls of mv-let, by
avoiding repeated evaluation of the expression to which its variables are
bound. Thanks to Sol Swords for requesting this improvement and sending an
Modified a heuristic to avoid the opening up non-recursive function calls
on calls of hide involving if-expressions. For example, the
thm form below is now admitted
(defun bar (x)
(cons x x))
(thm (equal (bar (hide (if a b c)))
(cons (hide (if a b c)) (hide (if a b c)))))
Fixed a soundness bug in destructor elimination, which was preventing some
cases from being generated. Thanks to Eric Smith for reporting this bug and
sending a helpful example. (Technical detail: the fixes were in ACL2 source
functions apply-instantiated-elim-rule and
eliminate-destructors-clause1, and comments in the former contain Eric's
Fixed a bug that supported a proof of 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
Changed the implementation of 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). (Thanks to Dave Greve for suggesting a reduction in the
warnings we produced related to 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.
Fixed a soundness bug related to 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
(defun f ()
(declare (xargs :guard t
(mv-let (a b c)
(mv 3 4)
(declare (ignore a b))
(defun g ()
(declare (xargs :guard t))
(prog2$ (mv-let (x y z)
(mv 2 3 4)
(declare (ignore x y z))
(equal (g) nil)
:hints (("Goal" :in-theory (disable (f))))
;;; Book top.lisp
:hints (("Goal" :use g-nil))
The modification described above pertaining to 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
(defun g (x) ; Use defun-nx to avoid an error after Version_3.6.1.
(declare (xargs :guard t :non-executable t))
(g 3) ; causes error, as expected
(g 3) ; returned 3 before the bug fix; after fix, causes error as expected
A hard error was possible when attempting to include an uncertified book
containing events of the form (make-event '(local ...)). This has
been fixed. Thanks to Sol Swords for bringing this issue to our
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)
(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))
(f 3) ; raw Lisp hard error
(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
(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
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
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
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
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.
(value-triple "Imagine something bad here!"))
(value '(value-triple :some-value)))
Formerly, the following commands succeeded.
(certify-book "test3" 0 t :ttags :all)
(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
Closed a small loophole that had the potential, in rare circumstances, to
violate atomicity of under-the-hood updates for ACL2 arrays.
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 non-locally inside an encapsulate event unless we determine that the proof obligations hold outside
the encapsulate event as well.
((f (x) t))
(local (defun f (x) (declare (xargs :guard t)) (consp x)))
(defun g (x)
(declare (xargs :guard (f x)))
The use of :comp on stobj functions had potentially
caused a hard Lisp error; for example, this could occur when (defstobj foo
fld) was followed by :comp foop. This has been fixed.
Fixed a bug that could cause a raw Lisp error when the first argument of
with-local-stobj is not a symbol.
It had been possible to use the reserved keyword
:computed-hints-replacement as the name of a custom keyword hint (see custom-keyword-hints). This has been fixed. Thanks to Dave Greve, who
pointed out a confusing hint error message (which has also been fixed) that
led us to this issue.
Fixed a bug that could cause a hard Lisp error, instead of a graceful ACL2
error, if keyword :backchain-limit-lst in a rule class is given a cons
that is not a true list, such as (1 . 1).
Eliminated an error that could occur when redefining a function as a macro
and then compiling, as in the example below.
(defun foo (x) x)
(defmacro foo (x) x)
Thanks to Eric Smith for sending the above example in his bug report.
Fixed a bug that could result in an assertion when a clause-processor causes an error.
NEW AND UPDATED BOOKS AND RELATED INFRASTRUCTURE
See the log
entries for a record of books changed or added since the preceding
release, with log entries.
We note in particular the new system/ directory, which begins to
specify ACL2 system code in anticipation of opening the architecture of ACL2
(see defattach for a relevant tool). Some system functions were
changed slightly (but with the expectation of not generally affecting ACL2
behavior) in support of the development of this directory. Those interested
in contributing to further such efforts are invited to contact the ACL2
New utilities have been provided for certifying most of the distributed
books with more `make'-level parallelism. 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
The top-level makefile, 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'
The HONS version, supported primarily by Bob Boyer and Warren Hunt (see
hons-and-memoization), has undergone numerous improvements. For
example, keyword argument :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. Thanks also to Jared Davis
for contributing structural modifications to the implementation of hons.
David Rager contributed modifications to the parallel version (see parallelism), which include taking advantage of atomic increments available
at least since Version 1.0.21 of SBCL and Version 1.3 of CCL.
- How to convert calls of wormhole for Version 4.0