|
|
|---|
|
|
|
|---|
ACL2 Version 8.4 (August, 2021) 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 to ACL2 since Version 8.3 into the following categories of changes: existing features, new features, heuristic and efficiency improvements, bug fixes, changes at the system level, 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 that only ACL2 system changes are listed below. See also note-8-4-books for a summary of changes made to the ACL2 Community Books
since ACL2 8.3, including the build system. Also note that with each release,
it is typical that the value of constant *ACL2-exports* has been
extended, and that some built-in functions that were formerly in
Apply$, lambda$, and loop$ may be used with badged
For calls of the form
The events defun-nx and defund-nx now disable
the executable-counterpart rune for the new function symbol.
Thus, after either of these introduces function symbol
Some built-in functions supporting the macro, position, now fix (coerce) their accumulator argument to a natural number. Thanks to Mihir
Mehta for supplying the initial such changes, for the purpose of avoiding
numeric type hypotheses. After that, thanks to email correspondence from
Warren Hunt, we added built-in
The macro defconst no longer accepts an optional documentation
string (which was already being ignored). Thanks to Eric Smith and Alessandro
Coglio for suggesting this change, which avoids potential confusion; consider
for example
Two improvements have been made in support of the case-match macro.
(1) The built-in constant *ACL2-exports* now includes the
A call of comment is more often inserted when the prover inserts a
call of hide. See comment for a discussion of such ways in
which
When a rewrite rule's conclusion is of the form
(defun my-equiv (x y) (equal x y)) (defequiv my-equiv) (in-theory (disable my-equiv)) ; optional (avoids warnings for the next form) (defthm foo (my-equiv x (car (cons x x))))
A trust tag (see defttag) is now required to set the ld-prompt to a non-Boolean value, other than the brr prompt, since that can cause printing of the prompt to modify state in rather arbitrary ways.
Improved translation of function calls, especially those that involve congruent stobjs, including better error messages, much improved code comments, and simplified code. Thanks to Sol Swords for sending an example with a misleading error message.
The error message has been improved when a
It is no longer an error to repeat a defun-sk event after removing
or adding the xargs declaration,
The set of apply$ primitives has been expanded. These are built-in
function symbols that do not need a warrant when reasoning about the
application of
Improved defwarrant to be a no-op for apply$ primitives.
ACL2 now points out when specious simplification takes place; see specious-simplification. Formerly this was the case only with gag-mode turned off; still,
For fmt directives
Reporting has been improved when encountering possible invariance violations for abstract stobjs. Now, when that happens an ``illegal-state'' is entered, as indicated by the prompt, and instructions are printed for how to proceed at your own risk. See illegal-state.
A table's guard may now reference the ACL2 state. Thus, it
may now be a term involving (at most) the variables
It is now always redundant to unmemoize a function symbol that is not currently memoized. See redundant-events.
The ``basic'' ruler-extenders (see rulers) now include not only the
symbols return-last and mv-list but also the symbol if. As before, the termination analysis always continues through the true
and false branches of
When supplying
It had been the case that if defun-nx or defund-nx is used
for a recursive definition, and that form specifies a value for
Improved handling of linear rules: cause an error with a helpful
message when a linear rule is no longer created during include-book or
the second pass of an encapsulate form, and optimize by avoiding
certain calculations when the
The event macros value-triple and assert-event have
been changed to be more flexible, in particular by providing an option to
allow the given form to return multiple values. They are also more efficient,
as they no longer evaluate using safe-mode by default.
(Technical note: As a consequence of implementation changes, one will rarely
if ever see ``hard'' errors (see er) from these utilities.) Thanks to
Eric Smith for requesting that a single utility encompass what is provided by
the built-in utility assert-event and the community-books
utilities assert! and assert!-stobj. That single utility is
now assert-event, which in turn uses
The ACL2 bdd package can now reason using the implicit rewrite rule
The event macro with-output has been improved with several
changes and new features (and correspondingly, so has
The value returned by a successful event
Two event macros produce much less output than before, as follows. Thanks to Alessandro Coglio for requesting these changes and to him and Eric Smith for helpful discussions.
For the
The utility set-guard-checking now prints messages to
In a proposed linear rule, hypotheses that are calls of bind-free are now accounted for when considering whether each of the
(defstub f (x) t) (defstub g (x) t) ; The following two events are the same except that the first supplies ; :trigger-terms while the second does not (instead computing trigger terms ; heuristically). These should either both fail or both succeed; now they ; both succeed. ; FAILED, but now SUCCEEDS after the fix since then variables y and z are ; considered to occur (free) in the hypotheses when determining ; whether the hypotheses and trigger term include enough variables to cover ; those in the conclusion. (defaxiom ax1 (implies (bind-free '((z . z))) ; or, (bind-free '((z . z)) (y z)) (< (f x) (g y))) :rule-classes ((:linear :trigger-terms ((f x))))) ; SUCCEEDED even before the fix: the bind-free hypothesis fools ACL2 ; into believing that otherwise-free variables may be bound by the ; bind-free alist. (defaxiom ax2 (implies (bind-free '((z . z))) ; or, (bind-free '((z . z)) (y z)) (< (f x) (g y))) :rule-classes :linear)
The report for
It is now an error for a
(defthm bad-rule (equal (< (foo x) x) nil) :rule-classes :linear)
In executable code, calls of hide in let-bindings or lambda bodies are no longer considered to represent ignore
declarations. We thank Alessandro Coglio for raising and discussing this
issue. Below is a log, based on that discussion, that was produced using ACL2
before this change. After this change, the second and third calls of
ACL2 !>:trans (let ((x 0)) (declare (ignore x)) 1) ((LAMBDA (X) '1) (HIDE '0)) => * ACL2 !>:trans ((LAMBDA (X) '1) (HIDE '0)) ; error after this change ((LAMBDA (X) '1) (HIDE '0)) => * ACL2 !>(untranslate '((LAMBDA (X) '1) (HIDE '0)) nil (w state)) (LET ((X (HIDE 0))) 1) ACL2 !>:trans (LET ((X (HIDE 0))) 1) ; error after this change ((LAMBDA (X) '1) (HIDE '0)) => * ACL2 !>
The defabsstobj keyword,
Strengthened error-checking for stobj-let to insist that if an
updater is supplied explicitly in a binding, then it must be a valid updater.
This check was formerly made only if the variable bound in that binding is
among the producer variables (see nested-stobjs). For example, the
following now causes an error, but it was formerly accepted in spite of the
fact that
(defstobj sub1 sub1-fld1) (defstobj top1 (top1-fld :type sub1)) (defun f1 (top1) (declare (xargs :stobjs top1)) (stobj-let ((sub1 (top1-fld top1) xyz)) ; bad updater! (val) (sub1-fld1 sub1) val))
The function symbol
The keyword
It is now possible to assign badges to
A new option for certify-book, provided with keyword option
A new keyword for defstobj,
The rewriter now rewrites the bodies of certain quoted lambda
objects. However, some restrictions apply. See rewrite-lambda-object.
In addition some new lemmas and a new metafunction have been added to the book
Added toggle-inhibit-warning and toggle-inhibit-warning! to
add or delete a warning string from the
It is now possible to instruct the prover to respect requests to disable the definition of the primitive, mv-nth, rather than continuing to expand that definition. See theories-and-primitives, in particular the note for advanced users at the end of that topic. Thanks to Alessandro Coglio for requesting this feature.
A new utility, memoize-partial, allows memoization for functions that were admitted by adding a formal parameter that decreases on each recursive call (sometimes called a ``limit'' or a ``clock''). Normally that extra parameter can severely impede the utility of memoization; however, the function actually executed does not have that extra parameter. This allows for more memoization hits. Thanks to Mertcan Temel for an inquiry leading to this enhancement, and for helpful discussions.
A new rule-class (see rule-classes) has been added, named
The loop$ parser produces more informative error messages on
ill-formed
A new memoize keyword,
A new xargs keyword for defun,
Tables may now supply custom error messages for table
The proof-builder command type-alist has a new optional argument that supports printing the type-alist in an alist format. Thanks to Mihir Mehta for requesting this feature.
A new summary type,
A
The
Stobj-let now allows aliases in the bindings in some cases where this is safe because updating is not involved. Thanks to Sol Swords for suggesting such a change.
Added a function ctxp to recognize valid contexts, which are used for printing error message (see ctx). Thanks to Eric Smith for requesting this addition and to Alessandro Coglio for suggesting that it be disabled, for efficiency.
The utilities brr and monitor now each take an optional
argument that avoids output. A new utility, monitor!, is a
combination of these two with their new optional arguments of
A new utility, get-guard-checking, returns the guard-checking value most recently installed, either
The function aset1-trusted may be used in place of aset1 to avoid invariant-risk, but is therefore untouchable.
Added a new utility, print-object$+, that is like print-object$ but instead of taking
We changed the lightweight ``preprocess'' simplifier for ``simple''
rules in the prover's waterfall, in the case that the term is the
application of a defined function symbol to constant (quoted) arguments. As
before, if the executable-counterpart rule for that function symbol is
enabled, then the call is evaluated in Lisp; and if that evaluation
fails (typically because a constrained function is called), then an attempt is
made to rewrite the term by applying a simple rule. The change is for
how failure is handled, that is, in the case that evaluation fails and the
term is not rewritten. Formerly, the term was surrounded by a call of hide. Now, that is only done by the main rewriter, not by the ``preprocess''
simplifier. Thanks to Eric Smith for a communication on the acl2-help list,
on a thread started by Mark Greenstreet, that led us towards making this
change. Mark's failed proof now succeeds after this change, but here is a
simpler example. Formerly, the commented-out
(defstub f (x) t) (defun g (x) (cons x (f x))) (thm (equal (car (g 3)) 3) ;; :hints (("Goal" :do-not '(preprocess))) )
The ACL2 rewriter has a ``being-openedp'' heuristic that prevents loops, by
saving a stack based on what is currently being rewritten. This can prevent
the use of a definition or rewrite rule. Now the heuristic is
turned off when the term's function symbol has a non-recursive definition and
simplification has just settled down (see hints-and-the-waterfall). To
restore the old behavior, i.e., to use the heuristic in all cases — thus
providing backward compatibility when a proof fails — evaluate the form:
When a command executed in a logical world,
Flushing current installed world. Reversing the new world. Installing the new world.
That process has been sped up significantly. Moreover, the new process avoids a bug reported by Eric Smith, who we thank for sending an example of how the process was interacting badly with reset-prehistory. Code implementing that interaction was introduced in Version 4.0 to speed up the process; that code has been eliminated, as it is no longer necessary.
ACL2's type-set reasoning has been slightly strengthened to
comprehend Boolean combinations of strong compound-recognizer calls on
a single variable when building a context (a so-called type-alist).
(By a ``strong compound-recognizer call'' we mean a unary function that
recognizes a union of primitive ACL2 types and has, either explicitly or
implicitly, a corresponding compound-recognizer rule; examples include
stringp, integerp, and true-listp.) In particular,
this change can strengthen the result of forward-chaining. Thanks to
Eric Smith, who raised this issue by providing an example that we include in a
comment, inside the form
Type-set reasoning also has been improved for inequalities to take
more advantage of the fact that the number 1 constitutes a singleton type.
For example, after evaluating
The function compress1 has been made more efficient in the following ways.
We found that accumulated-persistence was measurably slowing down ACL2 even when it is off. We modified its implementation and measured a time reduction of 3.7% for a proof-intensive book. The modification includes a documented efficiency tweak to wormhole-eval.
The linear-arithmetic heuristics have long taken advantage of negated equality hypotheses. These heuristics have been strengthened to take further such advantage. Thanks to Warren Hunt for sending an example proof attempt that failed before this change but now succeeds, and for his encouragement to pursue an improvement to linear arithmetic that can benefit such proof attempts.
The removal of guard-holders has been augmented to include removal of certain ``trivial'' lambda applications. See guard-holders, in particular for how to restore the legacy behavior. Thanks to Alessandro Coglio for an example and Eric Smith for a subsequent suggestion that led to this enhancement.
A soundness bug, present since loop$ was introduced, was fixed. The
bug was manifested when the keyword
A soundness bug was fixed by changing defabsstobj to avoid using
mbe in the definitions generated for the logic. The problem was that
the
A soundness bug was fixed in the functions that print to strings, such as
It was possible to prove
The mechanism for tracking warrants needed during a proof had a bug, which might be a soundness bug if one uses apply$ or loop$. That bug has been fixed.
Fixed a bug that was preventing use of the RDTSC hardware instruction in SBCL on most x86-based platforms, and possibly erroneously attempting to make use of that instruction on some other platforms. Thanks to Keshav Kini for a query that led to this fix. Also restricted RDTSC to x86-based platforms, thanks to a suggestion by Curtis Dunham, to enable Arm builds of ACL2.
The use of apply$ on calls of if no longer cause raw Lisp
errors. (The same is true for calls of the subroutine
We made the following fixes to the accumulated-persistence utility.
Fixed a bug that was causing books to be included as ``uncertified'' after their certification stored checksums (see book-hash). Thanks to Keshav Kini for reporting this bug.
ACL2 could occasionally simplify subterms of a call of hide even
without any applicable rules or
The notion of redundancy for defstobj events was too weak,
as evidenced by the following example. Consider the following book, named
(in-package "ACL2") (defstobj st fld) (defun foo (st) (declare (xargs :stobjs st)) (fld st))
After certifying this book, a raw Lisp error could occur after evaluating
the following forms, because the compiled definition of
(defstobj st fld :inline t) (include-book "bug") ; The defstobj event in this book is redundant here. (foo st)
The bug has been fixed by requiring a redundant defstobj event to be syntactically identical to the pre-existing corresponding defstobj event.
A raw Lisp error would occur when the value of an
Improved
The following defun-sk bugs were fixed.
For Lisps that do not compile on the fly (that is, Lisps other than CCL and
SBCL), evaluation of
When a stobj hash-table's ``init'' function was called with size 0, an error could occur for host Lisp GCL, complaining that size 0 is not allowed for hash-tables. This has been fixed by using size 1 instead of 0 in this case.
Reporting by break-rewrite has been fixed for cases when failure is
due to a hypothesis with a backchain-limit of 0. There were actually
two such bugs: one due to improper handling of linear rules (which
might have occurred even for other backchain-limits besides 0), and one due to
the erroneous assumption that backchaining has only just begun at the point of
failure. Thanks to Mihir Mehta for sending an example that exhibited both
bugs. A discussion of the second bug, including a simple example, may be
found in a comment in the ACL2 source function,
Fixed a bug in tracking the cbd that could cause failures of include-book in raw-mode. Thanks to Warren Hunt for a query leading to this fix.
Fixed a bug that was preventing some deep patterned-congruence rules from being applied. This could occur when on the left-hand side, the outermost function symbol is the same as the next function symbol going in towards the variable that differs on the right-hand side. Thanks to Mihir Mehta for reporting this bug and including a replayable example.
Fixed several issues with fmt (and related printing utilities)
pertaining to linebreaks. These include the following, many of which are
illustrated in a new file,
After setting state global
There are improvements to certify-book and include-book,
which pertain to the loading of compiled files by
Improved a utility that builds sets of clauses, which improves the
reliability of using a lemma-instance of the form
Fixed printing of the ACL2 state in error messages, specifically when executing a non-executable function.
Fixed a bug that could cause a raw Lisp error when processing a linear rule with a bind-free hypothesis, when that hypothesis does not specify a list of variables (in its second argument). Thanks to Dave Greve for reporting this bug by sending a simple example. (Technical note: the fix was in the definition of source function all-vars-in-hyps.)
For defabsstobj, a suitable error now occurs when the
An unfortunate ``Proof skipped'' could be printed during the
Fixed an implementation error that was being reported when a stobj-let form updates two array fields each with at least two indices that
are not all natural numbers. For an example that caused this error, see community-book
Fixed a bug in resizing stobj arrays whose elements are specified to
be
For a stobj-let call occurring in other than a definition body, the top-level bindings of variables to child stobj accessors was treated as let* rather than as let. That was at odds with the documentation, and has been fixed.
Fixed a bug that caused an error when attempting to redefine a function for
which a
Raw mode now does a better job of maintaining global stobj values. Here is an example that illustrates the fix; also see set-raw-mode, which has been extended to explain a related but remaining issue.
(defstobj st2 (ar :type (array t (8)) :resizable t)) (set-raw-mode-on!) (resize-ar 20 st2) (ar-length st2) ; formerly 8, but now 20 as expected
For any proof-builder command of the form
Consider when a community-book is included using an ACL2 executable
different from the one that certified the book, with those two executables
being located in different directories. The book is now considered to be
uncertified in that case. To avoid this issue see include-book for a
discussion of environment variable
(SBCL only) Filenames are now read as ASCII (specifically, ISO-8859-1) when the host Lisp is SBCL, which formerly was not the case. Thanks to Stephen Westfold for suggesting this change.
ACL2 can once again be built on CMU Common Lisp (CMUCL) (though we have
only done minimal testing). The problem turned out to be with ACL2, not
CMUCL: low-level Lisp code in the ACL2 sources was destructively modifying a
quoted constant. (For implementation details, see
There is now a way to save the untranslated bodies of built-in
Starting with ACL2 Version 7.0, the availability of hash consing (see
hons) and the other features described in hons-and-memoization
have been part of a default ACL2 build; meanwhile, support for ``classic''
ACL2 has essentially been discontinued. These features require a certain Lisp
action (implementation note: pushing
(SBCL only) Handling in ACL2 of the SBCL ``read-cycle-counter'' has been modified to reflect its handling in recent SBCL versions (starting around late 2018 or early 2019). This avoids an ACL2 build error on some platforms. Thanks to John R. Strohm for reporting such a problem (on a Raspberry Pi).
(SBCL only) Increased the number of special variables that can be created,
which allowed community book
Fixed builds that use a relative pathname for the LISP environment variable (for host Lisps CCL, SBCL, Allegro CL, and CMUCL; GCL and LispWorks didn't seem to have this problem). Thanks to Mihir Mehta for bringing this issue to our attention; and thanks to Andrew Walter for reporting a problem with our first solution for SBCL and proposing an alternative, which we adopted.
Fixed the process for running ACL2 without building an executable image. Some initialization that was missing from that process is now included. Also, added the missing command, (lp), to the instructions in section ``Running Without Building an Executable Image'' on the ``Obtaining and Installing ACL2'' web page (accessible from the ``Obtaining, Installing, and License'' link on the ACL2 home page). Thanks to Petter Gustad for an inquiry leading to these improvements.
When invoking `
The startup banner now has a cleaner look (see startup-banner). Thanks to Alessandro Coglio and Eric Smith for key suggestions for improvement.
(CCL only) When an attempt to build ACL2 fails, a more informative error message is printed when the error is caused by invoking CCL as a soft link on the Unix PATH rather than as a regular file. Thanks to Mertcan Temel for feedback leading to this change.
A script
When an error occurs while loading an ACL2-customization file, ACL2 quits with exit code 1. Thanks to Eric Smith for suggesting the quit and to Eric McCarthy for suggesting exit code 1 in that case.
ACL2 now does a more thorough job of doing proofs when ``
The ACL2-doc search commands (`
Highlighting in lisp-mode (inside Emacs) has been improved, both by
recognizing more keywords and by highlighting of some new arguments, in
particular the first argument of
The ACL2-doc browser now queries when first loading an ACL2+books manual if you have a newer web-based version. A ``yes'' response will use the (out-of-date) manual, while a ``no'' response will generally produce a new query asking if you want to download the manual from the web. This change was made in support of building the manual more quickly, as the acl2-doc manual is no longer built by default. See ACL2-doc for how to do that build and other details. Thanks to Alessandro Coglio, Eric Smith, and Sol Swords for discussions about speeding up the build of the manual.
Fixed certain hangs in the ACL2-doc browser. For example, when
standing on whitespace near the left margin of topic *ACL2-exports*,
the '
ACL2(p) now runs much more reliably on host Lisp SBCL (by taking advantage of a locking mechanism provided by SBCL). Thanks to David Rager for providing this improvement.
In ACL2(p), set-waterfall-parallelism no longer causes an error
when there are override-hints if the argument is the existing value of
the state global,