Major Section: RELEASE-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.3 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.
NOTE: ACL2 is now distributed under Version 2 of the GNU General Public License. [Added later: The license has changed since Version_5.0. See LICENSE.] Formerly, any later version had been acceptable. Moreover, books are no longer distributed from a University of Texas website, but rather, from Google Code at http://code.google.com/p/acl2-books/downloads/.
CHANGES TO EXISTING FEATURES
A fatal error now occurs if environment variable
ACL2_CUSTOMIZATION has a
value other than
NONE or the empty string, but is not the name of an
existing file. Thanks to Harsh Raju Chamarthi for requesting such a change.
main-timer are no longer untouchable
We now avoid certain duplicate conjuncts in the constraint stored for
encapsulate events. For example, the constraint stored for the
following event formerly included
(EQUAL (FOOP (CONS X Y)) (FOOP Y)) and
(BOOLEANP (FOOP X)) twice each, but no more.
(encapsulate ((foop (x) t)) (local (defun foop (x) (declare (ignore x)) t)) (defthm foop-constraints (and (booleanp (foop x)) (equal (foop (cons x y)) (foop y))) :rule-classes ((:type-prescription :corollary (booleanp (foop x))) (:rewrite :corollary (equal (foop (cons x y)) (foop y))))))
guard for a constrained function (see signature) may now
mention function symbols introduced in the same
encapsulate event that
introduces that function. Thanks to Nathan Wetzler for a helpful discussion
leading to this improvement.
The test for redundancy (see redundant-events) of
events has been improved in cases involving redefinition
(see ld-redefinition-action). Thanks to Jared Davis for providing the
following example, which illustrates the problem.
(redef!) (encapsulate () (defun g (x) (+ 3 x))) (g 0) ; 3, as expected (encapsulate () (defun g (x) (+ 4 x))) (g 0) ; 4, as expected ; Unfortunately, the following was flagged as redundant because it agreed ; with the first encapsulate above. That has been fixed; now, it is ; recognized as not being redundant. (encapsulate () (defun g (x) (+ 3 x)))
The test for redundancy of
defconst events has been
improved in the case that redefinition is active. In that case, redundancy
now additionally requires that the ``translated'' body is unchanged, i.e.,
even after expanding macro calls and replacing constants (defined by
defconst) with their values. Thanks to Sol Swords for requesting this
enhancement, and to Jared Davis for pointing out a bug in a preliminary
change. See redundant-events, in particular the ``Note About Unfortunate
Redundancies''. Note that this additional requirement was already in force
for redundancy of
defmacro-last and the table
been modified so that when they give special treatment to a macro
its raw Lisp counterpart
mac-raw, a call
(return-last 'mac-raw ...)
can be made illegal when encountered directly in the top level loop, as
opposed to inside a function body. See return-last. Thanks to Harsh Raju
Chamarthi for showing us an example that led us to make this improvement.
We removed a barrier to admitting function definitions, as we explain using the following example.
(defun foo (m state) (declare (xargs :stobjs state)) (if (consp m) (let ((state (f-put-global 'last-m m state))) (foo (cdr m) state)) state))Previously, ACL2 complained that it could not determine the outputs of the
LETform, as is necessary in order to ensure that
STATEis returned by it. ACL2 now works harder to solve this problem as well as the analogous problem for
MV-LETand, more generally for
mutual-recursion. (The main idea is to reverse the order of processing the
IFbranches if necessary.) We thank Sol Swords for contributing a version of the above example and requesting this improvement.
It is no longer the case that
break-on-error causes a Lisp break when
encountering an error during translation of user input into internal
(translated) form (see term). The reason is that an improvement to the
translation process, specifically the one described in the preceding
paragraph, allows certain backtracking from ``errors'', which are intended to
be silent rather than causing breaks into raw Lisp. Thanks to Jared Davis
for sending an example leading to this change.
(CCL and SBCL only) When the host Lisp is CCL or SBCL, then since all
functions are compiled, a
certify-book command will no longer load the
newly-compiled file (and similarly for
include-book with argument
Set-write-acl2x now returns an error triple and can take more values,
some of which automatically allow including uncertified books when
certify-book is called with argument :acl2x t.
The environment variable
COMPILE_FLG has been renamed
ACL2_COMPILE_FLG; see certify-book.
defund no longer return an error triple
:SKIPPED when proofs are being skipped. Rather, the value
returned is the same as would be returned on success when proofs are not
For those who use
set-write-acl2x: now, when
called without a
:ttagsx argument supplied, then the value of
defaults to the (explicit or default) value of the
pl2 commands can now accept terms
that had previously been rejected. For example, the command
:pl (member a (append x y)) had caused an error, but now it works as one
might reasonably expect, treating
(see equality-variants for relevant background). Thanks to Jared Davis for
reporting this problem by sending the above example.
We have eliminated some hypotheses in built-in rewrite rules
Added the symbols
Added to the guards of
remove-untouchable the requirement that the second argument must be a
Boolean. Thanks to Jared Davis for sending an example that led to this
The built-in function
string-for-tilde-@-clause-id-phrase has been put
logic mode and had its guards verified, as have some
subsidiary functions. A few new rules have been added in support of this
work; search for
string-for-tilde-@-clause-id-phrase in ACL2 source file
boot-strap-pass-2.lisp if interested. Thanks to David Rager for
contributing an initial version of this improvement.
All trust tags are now in the keyword package. The
may still take a symbol in an arbitrary package, but the trust tag created
will be in the keyword package (with the same
symbol-name as the symbol
provided). Similarly, non-
nil symbols occurring in the
argument of an
certify-book command will be
converted to corresponding keywords. See defttag.
There have been several changes to gag-mode. It is now is initially set
:goals, suppressing most proof commentary other than key checkpoints;
see set-gag-mode. (As before, see pso for how to recover the proof
output.) Also, top-level induction schemes are once again printed when
gag-mode is on, though these as well as printing of guard conjectures can be
abbreviated (``eviscerated'') with a new evisc-tuple;
see set-evisc-tuple, in particular the discussion there of
Finally, the commentary printed within gag-mode that is related to
forcing-rounds is now less verbose. Thanks to Dave Greve and David
Rager for discussions leading to the change in the printing of induction
schemes under gag-mode; thanks to Warren Hunt for an email that led us to
similar handling for printing of guard conjectures; and thanks to Robert Krug
for a suggestion that led us to restore, in abbreviated form, important
information about the sources of forcing round goals.
An error now occurs if
ld is called while loading a compiled book.
See calling-ld-in-bad-contexts. Thanks to David Rager for reporting a
low-level assertion failure that led us to make this change.
The proof-checker interactive loop is more robust: most errors will leave you in that loop, rather than kicking you out of the proof-checker and thus back to the main ACL2 read-eval-print loop. Thanks to David Hardin for suggesting this improvement in the case of errors arising from extra right parentheses.
The summary at the end of a proof now prints the following note when appropriate:
[NOTE: A goal of NIL was generated. See :DOC nil-goal.]See nil-goal.
dmr to show the function being called in the case of
explicit evaluation: ``
It is now permitted to bind any number of stobjs to themselves in the
bindings of a
LET expression. But if any stobj is bound to other than
LET bindings, then there still must be only one binding in
LET expression. The analogous relaxation holds for
expressions. Thanks to Sol Swords for requesting such a change, which was
needed for some code generated by macro calls.
top-level now returns without error; See top-level.
Formerly, this macro always returned an error triple
(mv t .. state),
which meant that normal calls of
ld would stop after encountering a
top-level. Thanks to Jared Davis for bringing this issue to our
It is no longer the case that when you specify
:non-executable t in a
defun form rather than using
then the form of the body need match only the shape
(prog2$ (throw-nonexec-error ... ...) ...). We now require that the body
of the definition of a function symbol,
fn, with formals
(x1 ... xk),
be of the form
(prog2$ (throw-nonexec-error 'fn (list x1 ... xk)) ...).
This fixes the following odd behavior, which could be considered a bug.
Consider a book that contains the following two events.
(defun foo (x) (declare (xargs :guard t :non-executable t :mode :logic)) (prog2$ (throw-nonexec-error 'bar (list x)) (cons 3 x))) (defn h (x) (foo x))After certifying this book and then including it in a new session, the behavior occurred that is displayed below; notice the mention of
BAR. However, if the two forms were submitted directly in the loop, then the error message had mentioned
BAR. This discrepancy has been eliminated, by rejecting the proposed definition of
foobecause the name in the first argument of
'barwhere now it must be
ACL2 !>(h 3) ACL2 Error in TOP-LEVEL: ACL2 cannot ev the call of undefined function BAR on argument list: (3) To debug see :DOC print-gv, see :DOC trace, and see :DOC wet. ACL2 !>
A tautology checker used in the ACL2 sources (function
been limited somewhat in the effort it makes to recognize a tautology. While
we expect it to be rare for the effect of this change to be noticeable, we
thank Sol Swords for sending us an example that motiviated this change: a
guard verification that took about 5 seconds in Version_4.3 now takes,
on the same machine, about 0.07 seconds.
The behavior of backquote (
`) has been changed slightly to be compatible
with its behavior in raw Lisp. The change is to allow the use of
,@) at the end of a list, as in the following example.
(let ((x 3) (y 2) (z 7)) `(,x ,y ,@z))Formerly, evaluation of this form had caused a guard violation in the ACL2 loop unless guard-checking was off (i.e.,
set-guard-checkingwas involked with
:none), in which case it returned
(3 2). But we observed evaluation of this form to return
(3 2 . 7)in every host Lisp on which ACL2 runs (Allegro CL, CCL, CLISP, CMUCL, GCL, LispWorks, and SBCL). Now, ACL2 behaves like these Lisps.
A call of the
theory macro had previously returned
nil when applied
to other than the name of name of a previously executed
event. Now, a hard error occurs.
binop-table has been replaced by the table
continue to have the same effect as before. See add-macro-fn, which is a new
feature discussed below.
booleanp is now defined using
eq instead of
equal, which may increase its efficiency. Thanks to Jared Davis for
(key . val) in the
macro-aliases-table, there had been a
val is a known function symbol. Now, it only needs to
be a symbol. (This change was made to support the new feature,
defun-inline, described elsewhere in these release notes.)
A new ``tau system'' provides a kind of ``type checker.'' See tau-system. Thanks to Dave Greve for supplying a motivating example (on which this system can provide significant speedup), and to Sol Swords for sending a very helpful bug report on a preliminary implementation.
Users may now arrange for additional summary information to be printed at the end of events; see print-summary-user. Thanks to Harsh Raju Chamarthi for requesting this feature and participating in a design discussion.
A new, advanced proof-checker command,
geneqv, shows the generated
equivalence relation at the current subterm. Thanks to Dave Greve for an
inquiry leading to this enhancement.
A new reader macro,
#u, permits the use of underscore characters in a
number. See sharp-u-reader. Thanks to Jared Davis for requesting this
New proof-checker commands
pr provide interfaces to the
pr, respectively. These can be
useful if you want to see trivially-proved hypotheses, as now clarified in
the proof-checker documentation for its
See proof-checker-commands. Thanks to Pete Manolios for suggesting such
clarification and capability.
It is now legal to call non-executable functions without the usual signature restrictions imposed on executable code. For example, the third event below was not admissible, but now it is.
(defstobj foo fld) (defun-nx id (x) x) (defun f (foo) (declare (xargs :stobjs foo :verify-guards nil)) (cons 3 (id foo)))Thanks to Jared Davis for requesting this enhancement, in particular for calling non-executable functions in the
:logicpart of an
mbecall. Here is Jared's example, which is admissible now but formerly was not.
(defstobj foo (fld)) (defun-nx my-identity (x) x) (defun my-fld (foo) (declare (xargs :stobjs foo)) (mbe :logic (my-identity foo) :exec (let ((val (fld foo))) (update-fld val foo))))
A new macro,
non-exec, allows the use of non-executable code, for
example inside ordinary function definitions. Thanks to Sol Swords for
requesting this enhancement.
A new ``provisional certification'' process is supported that can allow
books to be certified before their included sub-books have been
certified, thus allowing for potentially much greater `
parallelism. See provisional-certification. Thanks to Jared Davis for
requesting this feature and for helpful discussions, based in part on
rudimentary provisional certification schemes that he developed first at
Rockwell Collins and later for his `Milawa' project. Also, thanks to Jared
and to Sol Swords for testing this feature and for providing a fix for a bug
in a preliminary implementation, and thanks to Sol for providing performance
feedback and a crucial suggestion that led to an improved implementation.
Event summaries now show the names of events that were mentioned in
hints of type
See set-inhibited-summary-types. Thanks to Francisco J. Martin Mateos for
requesting such an enhancement (actually thanks to the community, as his
request is the most recent but this has come up from time to time before).
ACL2 now stores a data structure representing the relation ``Event A is used in the proof of Event B.'' See dead-events, which explains this data structure and mentions one application: to identify dead code and unused theorems. Thanks to Shilpi Goel for requesting such a feature and for helpful feedback.
A new documentation topic provides a guide to programming with state;
see programming-with-state. Thanks to Sarah Weissman for suggesting that
such a guide might be useful, and to David Rager for helpful feedback on a
preliminary version. There also has been some corresponding reorganization
of the documentation as well as creation of additional documentation (e.g.,
see state-global-let*). Now, most built-in functions and macros commonly
used in programs (as opposed to events like
defun, for example)
are subtopics of a new topic -- see acl2-built-ins -- which is a
subtopic of programming, a topic that in turn has considerably fewer
direct subtopiics than before.
It is now possible to bind extra variables in a
:USE hint, thus avoiding
the error message: ``The formula you wish to instantiate, ..., mentions only
the variable(s) ...''. See lemma-instance, in particular the discussion of
:extra-bindings-ok. Thanks to Sol Swords for requesting such an
read-object-suppress is like
read-object except that it
avoids errors and discards the value read. See io.
A stobj may now be passed as an argument where another stobj is expected
if the two are ``congruent''. See defstobj, in particular, its discussion of
:congruent-to keyword of
defstobj. Thanks to Sol Swords for
requesting this enhancement and for useful discussions contributing to its
A new top-level utility has been provided that shows the assembly language
for a defined function symbol; see disassemble$. Thanks to Jared Davis for
requesting such a utility and to Shilpi Goel for pointing out an
inconvenience with the initial implementation. Note that it uses the
books/misc/disassemble.lisp, which users are welcome to
modify (see http://www.cs.utexas.edu/users/moore/acl2/).
set-accumulated-persistence is an alias for
accumulated-persistence. Thanks to Robert Krug for suggesting this
A new documentation topic lists lesser-known and advanced ACL2 features, intended for those with prior ACL2 experience who wish to extend their knowledge of ACL2 capabilities. See advanced-features. Thanks to Warren Hunt and Anna Slobodova for requesting such information.
A new macro,
deftheory-static, provides a variant of
such that the resulting theory is the same at
include-book time as it
certify-book time. Thanks to Robert Krug for helpful
discussions on this new feature and for updating his
distributed books to use this feature.
A new event,
defabsstobj, provides a new way to introduce
single-threaded objects (see stobj and see defstobj). These so-called
``abstract stobjs'' permit user-provided logical definitions for
primitive operations on stobjs, for example using an alist-based
representation instead of a list-based representation for array fields.
Moreover, the proof obligations guarantee that the recognizer is preserved;
hence the implementation avoids executing the recognizer, which may be an
arbitrarily complex invariant that otherwise would be an expensive part of
guard checks. Thanks to Warren Hunt for a request leading us to design
and implement this new feature, and thanks to Rob Sumners for a request
leading us to implement a related utility,
See defabsstobj. Also thanks to Sol Swords for sending an example exhibiting
a bug in the initial implementation, which has been fixed.
A new command,
:psof <filename>, is like
:pso but directs proof
replay output to the specified file. For large proofs,
complete much more quickly than
pso. see psof. More generally,
a new utility,
wof (an acronym for ``With Output File''), directs
standard output and proofs output to a file; see wof.
The new macro
defnd defines a function with
disables that function, in analogy to how
defund defines with
defun and then disables. Thanks to Shilpi Goel for requesting
pl2 command now shows
linear rules; and a new
sls), is an
analogue of the proof-checker
sr) command, but
for linear rules. Thanks to Shilpi Goel for requesting this new
proof-checker command. Finally, a corresponding new proof-checker command,
al), is an analogue of the proof-checker
r) command, but for linear rules.
remove-macro-fn replace macros
remove-binop, respectively, though the latter
continue to work. The new macros allow you to decide whether or not to
display calls of binary macros as flat calls for right-associated arguments,
(append x y z) rather than
(append x (append y z)).
It is now possible to request that the host Lisp compiler inline calls of specified functions, or to direct that the host Lisp compiler not inline such calls. See defun-inline and see defun-notinline. We thank Jared Davis for several extensive, relevant conversations, and for finding a bug in a preliminary implementation. We also thank others who have engaged in discussions with us about inlining for ACL2; besides Jared Davis, we recall such conversations with Rob Sumners, Dave Greve, and Shilpi Goel.
Reading of ACL2
arrays (see aref1, see aref2) has been made more
efficient (as tested with CCL as the host Lisp) in the case of consecutive
repeated reads of the same named array. Thanks to Jared Davis and Sol Swords
for contributing this improvement.
Slightly modified the induction schemes stored, so that calls of so-called
``guard-holders'' (such as
prog2$ -- indeed, any call
return-last -- and
the) are expanded away. In particular,
calls of equality variants such as
member are treated as their
corresponding function calls, e.g.,
see equality-variants. Guard-holders are also now expanded away before
storing constraints for
encapsulate events, which can
sometimes result in simpler constraints.
Improved the performance of
dmr (technical note: by modifying raw Lisp
code for function
We now avoid certain rewriting loops. A long comment about this change,
including an example of a loop that no longer occurs, may be found in source
Slightly strengthened type-set reasoning at the level of literals (i.e.,
top-level hypotheses and conclusions). See the comment in ACL2 source
rewrite-atm about the ``use of dwp = t'' for an example of a
theorem provable only after this change.
Strengthened the ability of type-set reasoning to make deductions about
terms being integers or non-integer rationals. The following example
illustrates the enhancement: before the change, no simplification was
performed, but after the change, the conclusion simplifies to
Thanks to Robert Krug for conveying the problem to us and outlining a
(defstub foo (x) t) (thm ; should reduce conclusion to (foo t) (implies (and (rationalp x) (rationalp y) (integerp (+ x (* 1/3 y)))) (foo (integerp (+ y (* 3 x))))))
Fixed a class of soundness bugs involving each of the following functions:
serialize-read-fn, and (for the HONS version of ACL2)
clear-memoize-tables as well as (possible
serialize-write-fn. For example, we were able to admit
the following events, but that is no longer the case (neither for
as shown, nor analogously for other functions listed above).
(defthm not-true (stringp (cadr (getenv$ "PWD" (build-state)))) :rule-classes nil) (defthm contradiction nil :hints (("Goal" :in-theory (disable (getenv$)) :use not-true)) :rule-classes nil)
Fixed a soundness bug involving
with-live-state, which could cause an
error in the use of
delete-include-book-dir in a book or its portcullis commands.
See with-live-state, as the documentation for this macro has been updated; in
particular it is now untouchable (see remove-untouchable) and is intended
only for system hackers. Thanks to Jared Davis for reporting a bug in the
add-include-book-dir after our first attempt at a fix.
Fixed a soundness bug based on the use of
skip-proofs together with the
certify-book. An example proof of
nil appears in a comment in the ACL2 sources, in
(deflabel note-5-0 ...).
Fixed a soundness bug that allowed users to define new proof-checker
primitive commands. Before this fix, a book proving
nil could be
certified, as shown in a comment now in the introduction of the table
pc-command-table in source file
(Technical change, primarily related to
make-event:) Plugged a security
hole that allowed books' certificates to be out-of-date with
make-event expansions, but not recognized as such. The
change is to include the so-called expansion-alist in the certificate's
checksum. An example appears in a comment in the ACL2 sources, in
(deflabel note-5-0 ...).
Fixed a bug in guard verification due to expanding calls of primitives when translating user-level terms to internal form, so called ``translated terms'' (see term). While we have not observed a soundness hole due to this bug, we have not ruled it out. Before the bug fix, the following event was admissible, as guard verification succeeded (but clearly should not have).
(defun f () (declare (xargs :guard t)) (car (identity 3)))For those who want details about this bug, we analyze how ACL2 generates guard proof obligations for this example. During that process, it evaluates ground subexpressions. Thus,
(identity '3)is first simplified to
'3; so a term must be built from the application of
'3. Guard-checking is always turned on when generating guard proof obligations, so now, ACL2 refuses to simplify
'nil. However, before this bug fix, when ACL2 was building a term by applying
'3, it did so directly without checking guards; source code function
cons-termis `smart' that way. After the fix, such term-building reduction is only performed when the primitive's guard is met.
While calls of many event macros had been prohibited inside executable code, others should have been but were not. For example, the following was formerly allowed.
(defun foo (state) (declare (xargs :mode :program :stobjs state)) (add-custom-keyword-hint :my-hint (identity nil))) (foo state) ; Caused hard raw Lisp error!Thus, several event macros (including for example
add-custom-keyword-hint) may no longer be called inside executable code.
Fixed an assertion that could occur, for example, after reverting to prove
the original goal by induction and generating a goal of
NIL. Thanks to
Jared Davis for sending us a helpful example to bring this bug to our
It was possible for
defstobj to generate raw Lisp code with
excessively restrictive type declarations. This has been fixed. Thanks to
Warren Hunt for reporting this bug and sending an example that illustrates
it. See stobj-example-2 for examples of such raw Lisp code; now, one finds
(and fixnum (integer 0 *)) where formerly the type was restricted to
(integer 0 268435455).
Fixed a bug in that was ignoring the use of
certain cases involving a combination of computed hints and custom keyword
hints. Thanks to Robert Krug for reporting this bug and sending a very
Fixed a bug in the output from
defattach, which was failing to list
previous events in the message about ``bypassing constraints that have
been proved when processing the event(s)''.
(GCL only) Fixed a bug in
set-debugger-enable (which was only a bug in
GCL, not an issue for other host Lisps).
Fixed ACL2 trace output to indent properly for levels above 99 (up to 9999). Thanks to Warren Hunt for bringing this bug to our attention.
Fixed a bug in the reporting of times in event summaries -- probably one
that has been very long-standing! The times reported had often been too
small in the case of compound events, notably
Thanks to everyone who reported this problem (we have a record of emails from
Eric Smith and Jared Davis on this issue).
Fixed a bug in
:expand hints, where the use of
prevent other parts of such a hint. For example, the following invocation of
thm failed before this fix was made.
(defund foo (x) (cons x x)) (thm (equal (car (foo x)) x) :hints (("Goal" :expand (:lambdas (foo x)))))
Certain ``program-only'' function calls will now cause hard Lisp errors.
(The rather obscure reason for this fix is to support logical modeling of the
ACL2 evaluator. A relevant technical discussion may be found in source
oneify-cltl-code, at the binding of variable
There was an unnecessary restriction that
FLET-bound functions must
return all stobjs among their inputs. For example, the following
definition was rejected because
state was not among the outputs of
This restriction has been removed.
(defun foo (state) (declare (xargs :stobjs state)) (flet ((h (state) (f-boundp-global 'x state))) (h state)))
We fixed a bug, introduced in the preceding release (Version 4.3), in the check for irrelevant formals (see irrelevant-formals). That check had been too lenient in its handling of lambda (LET) expressions, for example allowing the following definition to be admitted in spite of its first formal parameter obviously being irrelevant.
(defun foo (x clk) (if (zp clk) :diverge (let ((clk (1- clk))) (foo x clk))))
Fixed a bug in the
mini-proveall target in
GNUmakefile. The fix
includes a slight change to the
:mini-proveall command (an extra
event at the end). Thanks to Camm Maguire for reporting this bug.
Fixed a bug that occurred when
certify-book was called after using
set-fmt-hard-right-margin to set a
small right margin.
set-inhibit-warnings so that it takes effect for a subsequent
include-book event. Thanks to Jared Davis and David Rager for queries
that led to this fix.
Hard Lisp errors are now avoided for certain
rewrite rules: those
whose equivalence relation is other than
equal when the rule is
originally processed, but is no longer a known equivalence relation when the
rule is to be stored. Thanks to Jared Davis for sending a useful example, a
minor variant of which is included in a comment in source function
Fixed a bug in the ACL2 evaluator (source function
was unlikely to be exhibited in practice.
Fixed a hard Lisp error that could occur for ill-formed
(:meta :trigger-fns '(foo)).
It is now an error to include a stobj name in the
Some bogus warnings about non-recursive function symbols have been eliminated
for rules of class
(Allegro CL host Lisp only) Fixed an obsolete setting of compiler variable
comp:declared-fixnums-remain-fixnums-switch, which may have been
responsible for intermittent (and infrequent) checksum errors encountered
while including books during certification of the regression suite.
Fixed a proof-checker bug that could result in duplicate goal names in
the case of forced hypotheses. An example showing this bug, before the fix,
appears in a comment in the ACL2 sources, in
(deflabel note-5-0 ...).
We fixed a bug in a prover routine involved in type-set computations involving linear arithmetic. This bug has been around since at least as far back as Version_3.3 (released November, 2007). We are not aware of any resulting unsoundness, though it did have the potential to weaken the prover. For example, the following is proved now, but was not proved before the bug was fixed.
(thm (implies (and (rationalp x) (rationalp y) (integerp (+ (* 1/3 y) x))) (integerp (+ y (* 3 x)))) :hints (("Goal" :in-theory (disable commutativity-of-+))))
Although all bets are off when using redefinition (see ld-redefinition-action), we wish to minimize negative effects of its use, especially raw Lisp errors. The examples below had caused raw Lisp errors, but no longer.
(defstobj st fld :inline t) (redef!) (defstobj st new0 fld) (u) (fld st) ; previously an error, which is now fixed ; Fresh ACL2 session: (redef!) (defun foo (x) x) (defmacro foo (x) `(quote ,x)) (u) ; Fresh ACL2 session: (redef!) (defmacro foo (x) (cons 'list x)) (defun foo (x) x)
Fixed a bug that could cause hard Lisp errors in an
Thanks to Sol Swords for sending an example that exhibited this bug. Here is
a simpler such example; the bug was in how it was checked whether the
guard for a guard-verified function (here,
g) depends on some
function introduced in the signature of the
encapsulate (here, the
(encapsulate ((f (x) t)) (local (defun f (x) (declare (xargs :guard t)) x)) (defun g (x) (declare (xargs :guard (if (integerp x) (f x) t))) x))
Fixed a bug in
mfc-relieve-hyp that we believe could prohibit its use on
the last hypothesis. Thanks to Sol Swords for reporting this bug and
providing a fix.
#! (see sharp-bang-reader) was broken after a skipped
readtime conditional. For example, the following input line caused an
#+skip #!acl2(quote 3)This bug has been fixed.
Fixed a bug in the break-rewrite utility, which was evidenced by error messages that could occur when dealing with free variables. An example of such an error message is the following; we thank Robert Krug for sending us an example that produced this error and enabled us to produce a fix.
HARD ACL2 ERROR in TILDE-@-FAILURE-REASON-PHRASE1: Unrecognized failure reason, ((MEM-ARRAY . X86) (ADDR QUOTE 9)).
We fixed an obscure bug that we believe could interfere with
because of an incorrect
(declaim (notinline <function>)) form.
CHANGES AT THE SYSTEM LEVEL AND TO DISTRIBUTED BOOKS
Improvements have been made related to the reading of characters. In
particular, checks are now done for ASCII encoding and for the expected
char-code values for
Rubout. Also, an error no longer occurs with certain uses of
non-standard characters. For example, it had caused an error to certify a
book after a single portcullis command of
(make-event `(defconst *my-null* ,(code-char 0))); but this is no longer
an issue. Thanks to Jared Davis for helpful correspondence that led us to
make these improvements.
The character encoding for reading from files has been fixed at iso-8859-1. See character-encoding. Thanks to Jared Davis for bringing this portability issue to our attention (as this change arose in order to deal with a change in the default character encoding for the host Lisp, CCL), and pointing us in the right direction for dealing with it. In many cases, the character encoding for reading from the terminal is also iso-8859-1; but this is not guaranteed. In particular, when the host Lisp is SBCL this may not be the case.
Although the HTML documentation is distributed with ACL2, it had not been
possible for users to build that documentation without omitting graphics, for
example on the ACL2 home page. That has been fixed, as files
graphics/*.gif are now distributed.
Compiler warnings are suppressed more completely than they had been before. For example, the following had produced a compiler warning when the host Lisp is CCL, but no longer does so.
(defun f () (car 3)) (trace$ f)
Removed support for ``tainted'' certificates. One reason is that there are rarely incremental releases. A stronger reason is that for the compatibility of a new release is with the previous non-incremental release, it's not particularly relevant whether or not the new release is incremental.
The `make' variable
BOOKS can now be defined above the line that includes
Makefile-generic. (For relevant background, see book-makefiles.)
(SBCL only) ACL2 images built on SBCL now have an option,
--dynamic-space-size 2000, that can avoid space problems that could
previously have caused the session to die.
The default value for variable
LISP in file
GNUmakefile is now
ccl. Thus, if you use `
make' in the standard way to build an ACL2
executable, the default host Lisp is
ccl rather than
For the version supporting the reals, ACL2(r) (see real), the supporting
floor1 has been defined in raw Lisp. This avoids an error
such as in the following case.
(defun f () (declare (xargs :guard t)) (floor1 8/3)) (f) ; had caused raw Lisp error, before the fix
Among the enhancements for the parallel version, ACL2(p) (see parallelism), are the following. We thank David Rager for his work in developing ACL2(p) and these improvements in particular.
set-parallel-evaluationhas been renamed
Calls of the macro
set-waterfall-printingare no longer events, so may not be placed at the top level of books. However, it is easy to create events that have these effects; see set-waterfall-printing. Note that now,
ubtand similar commands do not change the settings for either waterfall-parallelism or waterfall-printing.
The implementation of
deflockhas been improved. Now, the macro it defines can provide a lock when invoked inside a guard-verified or
programmode function. Previously, this was only the case if the function definition was loaded from raw Lisp, typically via a compiled file.
The underlying implementation for waterfall parallelism (see set-waterfall-parallelism) has been improved. As a result, even the largest proofs in the regression suite can be run efficiently in
:resource-basedwaterfall parallelism mode. Among these improvements is one that can prevent machines from rebooting because operating system limits have been exceeded; thanks to Robert Krug for bringing this issue to our attention.
There is also a new flag for configuring the way waterfall parallelism behaves once underlying system resource limits are reached. This flag is most relevant to
:fullwaterfall parallelism. see set-total-parallelism-work-limit for more information.
dmrutility has the same behavior in ACL2(p) as it has in ACL2 unless waterfall-parallelism has been set to a non-
nilvalue (see set-waterfall-parallelism), in which case statistics about parallel execution are printed instead of the usual information.
The user can now build the regression suite using waterfall parallelism. See the distributed file
acl2-customization-files/READMEfor details, and see unsupported-waterfall-parallelism-features for a disclaimer related to building the regression suite using waterfall parallelism.
When building ACL2 with both the hons and parallelism extensions (what is called ``ACL2(hp)''), the functions that are automatically memoized by the hons extension are now automatically unmemoized and memoized when the user toggles waterfall parallelism on and off, respectively.
set-waterfall-parallelismwith a flag of
tnow results in the same settings as if it were called with a flag of
:resource-based, which is now the recommended mode for waterfall parallelism. Thanks to Shilpi Goel for requesting this feature.
The prover now aborts in a timely way in response to interrupts issued during a proof with waterfall parallelism enabled. (This had often not been the case.) Thanks to Shilpi Goel for requesting this improvement.
Among the enhancements for the HONS extension (see hons-and-memoization) are the following.
The compact-print code has been replaced by new serialization routines contributed by Jared Davis. This may improve performance when including books that contain
make-events that expand to very large constants. You can also now save objects to disk without going into raw lisp; see serialize for details.
Printing of certain messages has been sped up (by using Lisp function
force-outputin place of
finish-output). Thanks to Jared Davis for contributing this improvement.
Stobj array writes are perhaps twice as fast.
It is now permitted to memoize functions that take user-defined stobjs as inputs, provided that no stobjs are returned. Even if stobjs are returned, memoization is permitted provided the condition is
nil, as when profiling (see profile). Thanks to Sol Swords for an observation that led to this improvement and for useful conversations, including follow-up leading us to improve our initial implementation.
Fixes have been made for memoizing with a non-
:ideal-okp. Errors had occurred when memoizing with a
logicmode function that had not been guard-verified, even with a non-
:ideal-okp; and after successfully memoizing such a function (without such
:condition), it had not been possible to
unmemoizeit. Thanks to Sol Swords for reporting issues with the
If a book defined a function that was subsequently memoized in that book, the function would no longer behaves as memoized upon completion of book certification (unless that
certify-bookcommand was undone and replaced by evaluation of a corresponding
include-bookcommand). This has been fixed. Thanks to David Rager for pointing out the problem by sending an example.
We now support ACL2(h) built not only on 64-bit CCL but also on all supported host Ansi Common Lisps (i.e., all supported host Lisps except GCL). Thanks to Jared Davis for doing much of the work to make this improvement. Note that performance will likely be best for 64-bit CCL; for some Lisps, performance may be much worse, probably depending in part on the underlying implementation of hash tables.