ACL2 Version 8.6 (xxx, 20xx) 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.5 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-5-books for a summary of changes made to the ACL2 Community Books
since ACL2 8.5, 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
The connected book directory (that is, the cbd) now elaborates
relative pathnames to absolute pathnames not only for book operations,
but for all file operations. For example,
The proof-builder now takes into account various aspects of rewriting specified by the logical world that it formerly ignored (pertaining to match-free, case-split-limitations, untouchable functions, non-linear arithmetic (see set-non-linearp), the backchain-limit for rewriting, and the rw-cache-state).
The macro warrant now forces the warrants listed.
The utility read-file-into-string has been improved in the following ways.
The trace$ option
The use of
Warnings for non-recursive functions in left-hand sides of rewrite rules (similarly for linear, forward-chaining, and type-prescription rules) now consider bodies of lambda objects that could be rewritten (see rewrite-lambda-object).
The output is more informative when
The definition of pseudo-termp has been simplified by dropping a
superfluous true-listp check. Thanks for the suggestion from Eric
Smith. A new lemma,
The failure message regarding useless-runes (see useless-runes-failures) has been restricted to the case that a proof was attempted by the event (though there may be rare exceptions). Thanks to Eric Smith for requesting such a change.
Certain guard proof obligations for
The rewriter has been changed to handle certain calls of
A few new lemmas have been added to the standard
Time-limit and theory-invariant errors may now be inhibited
much as step-limit errors, by using
A new command,
The documentation for redundant-events includes the following, which
however was not enforced when the new event is in
4. If either the old or new event is a mutual-recursion event, then redundancy requires that both are mutual-recursion events that define the same set of function symbols.
A new feature, called ``transparent'' functions, can allow one to avoid the
restriction on a rule of class
When there an attachment to a common ancestor of the evaluator and meta
function of a proposed rule of class
A new walkabout command,
Arranged that iprinting that takes place during break-rewrite
or cw is better reflected outside break-rewrite. For examples, see
community-books input file
When a defined function has a declare form with
It had been the case that for type declarations of flet
definitions in a surrounding defun form, they were dropped in the
The behavior of pso and related utilities (pso!, psof, and psog) has been modified to avoid introducing warnings that
were not originally printed. For example, the output generated by
(set-inhibit-output-lst '(warning proof-tree)) (defthm foo t :hints (("Goal" :use car-cons)) :rule-classes nil) :pso
The above change has additional, small output effects, probably for the
better. For example, output from the form
ACL2 Error [Failure] in ( THM ...): See :DOC failure.
When an event fails, then if it involves definition runes for loop$ scions, the failure message may suggest including the book
Replaced length calls in the defun of pseudo-termp with
calls of a new macro,
When there is an error from evaluation of a form encountered by ld,
in a session where the value of ld-error-triples is the default of
This behavior was already present in the case that the “error on evaluation” was from an evaluation result
(mv erp val state)where erpis non- nil; but it has been extended to the case that erpis niland valis of the form (:STOP-LD . x), as is returned by default by ldupon an evaluation error. A key effect of this change is for the case that a .acl2file produces an error from a call of build::cert.pl. The following example illustrates; explanation follows below.;;; foo.acl2 (ld '((defun g (x) y)) :ld-error-action :return!) ;;; foo.lisp (in-package "ACL2")
Before this change, the command ‘
cert.pl foo’ resulted in a hard Lisp error (as seen in foo.cert.out). To see why, first note that cert.plexecutes a sequence of commands as follows (several omitted as shown with “ ...”).... (set-ld-error-action (quote (:exit 1)) state) ... ; instructions from .acl2 file foo.acl2: (ld '((defun g (x) y)) :ld-error-action :return!) ... #!ACL2 (set-ld-error-action (quote :continue) state) ...
The call of
ldabove returns (mv nil (:STOP-LD 2) state). Because ld-error-actionat the top level no longer has the default value of :CONTINUE, that result is considered an error (see ld-error-action) and top-level evaluation halts. Before this change, then ACL2 did not quit since the value was of the form (mv nil _ state); instead, ACL2 would quit the top-level call of ld, leaving us in raw Lisp. But in raw Lisp, the #!reader macro (see sharp-bang-reader) is undefined; hence an error would be signalled. After the fix, the return value of (mv nil (:STOP-LD 2) state)is treated as an error, so because ld-error-actionis (:EXIT N), ACL2 immediately exits with status N.
The pretty-printer has been improved by a contribution from Stephen Westfold to support appropriate indentation, including more conventional pretty-printing for calls of common macros such as defun and defmacro. See ppr-special-syms; we thank Stephen also for supplying the substance of that documentation. Thanks too to Stephen for suggesting several user-defined macros to be pretty-printed with this mechanism, which we have modified by adding suitable table events (e.g., for define).
Runtime guard violation messages from
Four obsolete fields of the ACL2 state have been removed:
Improved hide calls in prover output from failed execution of warrants, by adding suitable notes about attachments or warrant functions not being executable during proofs. Thanks to Eric McCarthy for a remark that led to this change.
The macro state-global-let* no longer requires explicitly supplying a setter for certain built-in state global variables. See state-global-let*.
A proposed defaxiom event is no longer redundant with
an existing defthm event. Before this change, the following book
could (perhaps unfortunately) be certified, even without certify-book
(in-package "ACL2") (local (defthm foo (equal (car (cons x x)) x))) (defaxiom foo (equal (car (cons x x)) x))
The prover sometimes reduces a goal without hypotheses (technically
speaking, a one-element clause) to
The default for memoize keyword argument
When a proof attempt is halted so that it reverts to prove the original
goal by induction, the top-level checkpoints are printed under the summary under the banner, “
For most built-in tables, improved error messages for guard failures. This improvement was made by using a new macro that is also available to ACL2 users, set-table-guard, which adds a table guard that produces a user-friendly error message when the guard fails.
The prover may now print a parenthetical remark about “dropping false conclusion”. That remark points to a new documentation topic, which provides explanation: see clause.
The new zero-ary attachable system function, heavy-linear-p, allows
for enhanced use of linear-arithmetic during rewriting, specifically
with the test (first) argument of a call of
There is a new `
New utilities get-cpu-time and get-real-time return the cpu time and real (wall clock) time that has elapsed since the start of the ACL2 session. Thanks to Eric McCarthy for suggesting the addition of such utilities.
The new utility er-hard is analogous to er-soft, but for hard errors instead of soft errors (see er).
A new command,
A directory of books may now be relocated so that those books are
still treated as certified. This is supported by a new project-dir-alist, which associates keywords with ``project directories'' and
is set using environment variable
A new break-rewrite command,
It is now possible to cause make-event to do proofs during its expansion phase even in a context where proofs are generally skipped (see ld-skip-proofsp). See make-event, in particular the discussion there labeled as “(4)”. Thanks to Eric Smith for requesting such a feature.
The induction mechanism in the prover can now deduce induction suggestions
(defthm acl2-count-car-cdr-linear (implies (consp x) (equal (acl2-count x) (+ 1 (acl2-count (car x)) (acl2-count (cdr x))))) :rule-classes :linear)
The Common Lisp utility, macrolet, is now supported in ACL2. Thanks to Alessandro Coglio for discussion leading us to make this addition. See macrolet.
The new utility with-cbd creates a scope for an indicated value of
the connected book directory (see cbd). Calls of
The new utility, with-current-package, evaluates a given form with respect to an indicated current-package. Thanks to Sol Swords for requesting this utility.
See fast-cert for a “fast-cert” mode for faster, but possibly unsound, book certification, in particular when using a saved executable that contains local events. Thanks to Sol Swords for requesting such a capability and for helpful design discussions.
Added utility set-warnings-as-errors, which can change warnings to hard errors. Thanks to Mark Greenstreet for the idea and for discussions that were helpful in refining it.
A new ld special, ld-always-skip-top-level-locals, has the
effect of skipping local top-level forms. Thanks to Sol Swords for
requesting such a capability, to support faster loading of
It is now permitted for a stobj
A new utility, with-brr-data, together with related query utilities,
allows one to find the source of a term in prover output. Thanks to Sol
Swords for requesting something like this in 2008 (!) and to Eric Smith for
requesting a related utility (see community-books
Added a “desperation heuristic” to compute a stronger context, for the extra try at simplification made after a goal is not changed by simplification. Thanks to Warren Hunt and Vivek Ramanathan for supplying an example of a theorem whose proof had a surprising failure but now succeeds. (Technical Remark describing this change: When a clause has most recently settled down at the time that the simplify process is invoked (a so-called “desperation heuristics” attempt), then the literals are reordered before building the type-alist, so that the literals that involve at most one variable precede the other literals.)
Generation of guard clauses (and, probably rarely, other goals) has been sped up in certain extreme cases. For details, see system-attachments, specifically the discussion of CONJOIN-CLAUSE-SETS-BOUND in the “Summary of attachable system functions”. Thanks to Alessandro Coglio for sending an example that led to our discovery of the quadratic behavior eliminated by this change.
Duplicate entries in type-alists (proof contexts) are now avoided in
many cases. (Implementation note: some calls extending the type-alist with an
existing term/type-set pair are now avoided in source function
Sped up macroexpansion for several common macros, with roughly a 2% to 3% speedup observed for including several large books during development of this change.
Tweaked linear-arithmetic to avoid consideration of an equality between two terms that are both known (via their type-sets) to be non-numeric.
The utility set-cbd is more efficient when setting to the current
cbd, including the common case of calls to
Fixed a soundness bug based on rules of class
It was probably a soundness bug to allow a defaxiom event to
designate a rule of class
The function read-file-into-string has been modified to avoid what
might be considered a soundness bug. The change involves causing an error for
two reads of the same file without first incrementing the file-clock of the
state. See read-file-into-string for details, in particular for
how to avoid that error by evaluating
First run the following shell commands.echo 'test1' > tmp1.txt ; echo 'test2' > tmp2.txt cp -p tmp1.txt tmp.txt
Then start ACL2 and run a command as follows.ACL2 !>(read-file-into-string "tmp.txt") "test1 " ACL2 !>
Now suspend ACL2 with
control-Zand run the following shell command.cp -p tmp2.txt tmp.txt
Now resume ACL2 with
fg, and optionally submit some trivial form (say, 3) just to get the prompt back. Note that the file-clock of the statehasn't changed. (Probably the statehasn't changed; at any rate, the parts of the state relevant to read-file-into-stringhaven't changed.) So the following call has arguments identical to those in the corresponding call above, yet yields a different result.ACL2 !>(read-file-into-string "tmp.txt") "test2 " ACL2 !>
After the change to
read-file-into-string, its call just above causes an error.
Fixed a bug in system function
Consider calls of defthm and thm that create subgoals
before reverting to prove the original goal by induction. The Rules summary
printed at the end should exclude rules used only before the start of that
induction proof. That was formerly the case for
(thm (equal (append (append x y) z) (append x y z)) :hints (("Goal" :expand ((:free (b) (append x b)) (:free (a b) (append (cons (car x) a) b))))))
Fixed bugs in the definition of source macro
Fixed translation of
Several improvements were made to the
ACL2 !>(loop$ for tail of-type cons on '(a b c) collect tail) ACL2 Error [Evaluation] in TOP-LEVEL: The guard condition (CONSP LOOP$-LAST-CDR), which was generated from a type declaration, has failed. See :DOC set-guard-checking for information about suppressing this check with (set-guard-checking :none), as recommended for new users. To debug see :DOC print-gv, see :DOC trace, and see :DOC wet. ACL2 !>Corresponding run-time checking was added for the types of the lower and upper bounds
Fixed a low-level bug in source function
(defun foo (n) (apply$ (lambda$ (x) (declare (type (signed-byte 8) x) (xargs :guard (signed-byte-p 8 x) :split-types t)) (+ 3 x)) (nfix n)))
Suppose a book is certified in a world where a portcullis
command generates a local call of make-event. Then
that event is now ignored when subsequently including that book. Previously
it may not have been ignored, because the
Some handling of exceptional cases in hints has been cleaned up, as follows. Thanks to Eric Smith for a discussion that led to these changes.
A bug in the brr commands
When a certified book is included, the logical world will no longer
be marked as having seen a skip-proofs call, even when the value of
ld special ld-skip-proofsp is non-
Fixed a bug that was causing calls of wormhole to signal an error.
Fixed a bug that could cause a do-loop$ expressions to be inappropriately rejected due to an allegedly ignored variable. An example is below.
(include-book "projects/apply/top" :dir :system) ; BUG: The following was formerly necessary, but no longer is. (set-ignore-ok t) (defun f (a b) (loop$ with x = a with y = b do ; The use of (set-ignore-ok t) was needed, but shouldn't have been, ; whether or not the next line is included. :measure (+ (len x) (len y)) (cond ((consp y) (let ((z y)) (progn (setq y (cdr x)) (setq x (cdr z))))) (t (return y)))))
Fixed the failed redundancy check when setting a table guard that
returns two values. For example, the form
Fixed a bug that was causing cw-gstack to report “Rewriting (to simplify) the first argument” when rewriting the second argument of a call of implies, and fixed an analogous bug for return-last.
Implementations underlying the functions sys-call, sys-call+, and sys-call* have been cleaned up. In particular, we now
expect them to indicate precisely the case of a non-error process return as
follows: 0 for sys-call-status, and
Significantly extended documentation topic system-attachments, which now lists all built-in system attachments, many with brief documentation. Thanks to Eric Smith for suggesting this enhancement.
Significant new documentation topics, together with subtopics and books supporting those topics, include the following. Note that for all but the their release was approved by DARPA with “DISTRIBUTION STATEMENT A. Approved for public release. Distribution is unlimited.”
Allow ld output in raw-mode to go to other than the channel,
A set of tools for assisting in the conversion of certain HTML to xdoc may be found, without much documentation, in
When new ACL2-doc buffers are created by using the
The initialization file for recent Emacs versions,
Documentation printed to the terminal or in the ACL2-Doc Emacs browser can respect certain xdoc::markup that was formerly ignored, but is no longer (by default): for example, text marked as underline is now underlined, and text marked as having typewriter font now has a grey background. This closes GitHub Issue 1487. Thanks to Grant Jurgensen for helpful feedback on the original plan, which had been to use delimiting underscores rather than Select Graphic Rendition (SGR) control sequences. See xdoc::terminal for details and for ways to customize behavior, including avoidance of SGR.
The note “Note: No checkpoints to print.” that might be printed on proof failure is now the same in ACL2(p) as in ACL2, unless waterfall-parallelism is enabled (in which case “no checkpoints” is followed by “ from gag-mode” as before).