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 @(tsee mutual-recursion) event, then redundancy requires that both are @(tsee 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
is better reflected outside break-rewrite. For an example, see the example on
iprinting in a comment in the form
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 pp-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).
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
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
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.
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)))))
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 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
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).