		Search-engine friendly clone of the ACL2 documentation.

Release-notes

Note-8-6

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 :program mode are now guard-verified :logic mode functions.

Changes to Existing Features

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, (open-input-channel "foo" :character state) now interprets filename "foo" relative to the cbd, where formerly it was generally interpreted relative to the directory in which ACL2 was invoked. (Technical note: ACL2 accomplishes the new behavior by arranging that set-cbd modifies not only the cbd but also the Lisp global, *default-pathname-defaults*.) Thanks to Alessandro Coglio, Eric McCarthy, and Eric Smith for suggesting consideration of such a change and for helpful discussions.

The function hons-enabledp is no longer defined, and :hons has been removed from the Lisp global, *features* (so, readtime conditionals #+hons and #-hons should be avoided, especially since #+hons is always false even though the system is hons-enabled). These were both deprecated in the preceding release (ACL2 Version 8.5). Note that the hons-enabled features of ACL2 have been included in all builds by default since Version 7.0 (January, 2015) and in all builds since Version 7.2 (January, 2016).

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 utilities set-inhibit-er-soft, set-inhibit-er-soft!, toggle-inhibit-er-soft, and toggle-inhibit-er-soft! have been renamed by dropping the suffix ``-soft'', hence they are now the following, respectively: set-inhibit-er, set-inhibit-er!, toggle-inhibit-er, and toggle-inhibit-er!. The relevant table has similarly been renamed from inhibit-er-soft-table to inhibit-er-table. These changes reflect their relevance for the new utilities, er-hard and er-hard, in addition to er-soft.

The macro warrant now forces the warrants listed.

:Induction rules now support the use of syntaxp hypotheses.

The utility read-file-into-string has been improved in the following ways.

The value of the :start argument may now be any natural number less than the length of the input file. (Formerly one needed to use this utility to read the preceding bytes first, which can be much slower.) Thanks to Eric McCarthy, Eric Smith, and Grant Jurgensen for requesting this improvement and for helpful discussions.
While the default behavior is the same for when the corresponding Lisp stream is closed, a new keyword argument, :close, can be supplied to control that behavior.
Miscellaneous clean-up has been made in the implementation.
Restrictions have been tightened a bit to avoid what could be considered a soundness bug. See discussion about that in the section on “Bugs” below.

The trace$ option :evisc-tuple :print, which continues to use raw Lisp printing, has undergone the following improvements when printing entry and exit values. Thanks to Eric McCarthy for a query that led to these improvements.

Values are now pretty-printed.
Array values are no longer displayed as stobjs. (This includes stobjs themselves, since they are arrays.)

The use of (:executable-counterpart rewrite-lambda-modep) to control the behavior of lambda object rewriting by the prover (see rewrite-lambda-object) has been elaborated.

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 :pr is applied to an undefined primitive, such as car or binary-+, or a macro-alias for one of those, such as +. Thanks to Eric Smith for pointing out odd output for examples like :pr binary-+.

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, pseudo-termp-consp-forward, has been added to prevent some existing proofs from failing due to the change.

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 DO loop$s (so-called special conjectures (e), (f), and (g)) have been combined into one conjecture with a conjunction of three conditions in the conclusion to speed up proofs. See the comment starting with ``Special conjectures (e), (f), and (g)'' in the function special-conjectures in the source file history-management.lisp.

The rewriter has been changed to handle certain calls of ev$ faster. See rewriting-calls-of-apply$-ev$-and-loop$-scions.

A few new lemmas have been added to the standard apply$ book to simplify applications of assoc-equal-safe faster.

Time-limit and theory-invariant errors may now be inhibited much as step-limit errors, by using (set-inhibit-er "Time-limit") or (set-inhibit-er "Theory"), respectively. Thanks to Eric Smith for requesting this enhancement and its use in the implementation of the utility, prove$.

A new command, (cmds c1 c2 ... cn), has been added to walkabout.

The documentation for redundant-events includes the following, which however was not enforced when the new event is in :program mode; that has been fixed.

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 :meta or :clause-processor that there are no common ancestors of its evaluator and meta function. See evaluator-restrictions for relevant background, and see transparent-functions for documentation of the new feature. Thanks to Mertcan Temel for requesting a way to work around that restriction, and thanks to Sol Swords for suggesting (and naming) the notion of transparent functions. We are also grateful to Sol for providing a very helpful sketch of a correctness proof.

When there an attachment to a common ancestor of the evaluator and meta function of a proposed rule of class :meta or :clause-processor, the resulting error message now includes ancestor paths leading from the evaluator or meta function to a common ancestor.

A new walkabout command, up, moves up a level and exits the walkabout loop when already at the top level. It is thus equivalent to the existing command, 0, which is still supported although up is highlighted in the documentation; see walkabout). Thanks to Eric Smith for suggesting up.

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 (defxdoc note-8-6 ...) in community-book books/system/doc/acl2-doc.lisp.

When a defined function has a declare form with (optimize ...), that is now included in a declare form of the executable-counterpart function (see evaluation), which had not been the case.

It had been the case that for type declarations of flet definitions in a surrounding defun form, they were dropped in the defun form's executable-counterpart (see evaluation). Now they are included.

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 :pso below no longer prints the warning that had been suppressed for the defthm event below.

(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 (with-output :off (error summary) (thm (equal x y))) no longer prints the line shown below (at the end).

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 projects/apply/top if it hasn't already been included. That book provides quite a few lemmas about loop$ scions.

Replaced length calls in the defun of pseudo-termp with calls of a new macro, len$, which is a call of mbe that invokes length in the :exec code and len in the :logic code. Thanks to Eric Smith for requesting such an enhancement, and for discussing specifics of it, so as to avoid the need for at least one unfortunate rule that if (pseudo-termp term) then (not (stringp (cdr term))), apparently needed because length behaves specially on strings.

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 t and the value of ld-error-action is of the form (:EXIT N), then ACL2 quits with exit status N in some cases where formerly it did not. The following explanation is rather technical; see ld-error-action for relevant background.

This behavior was already present in the case that the “error on evaluation” was from an evaluation result (mv erp val state) where erp is non-nil; but it has been extended to the case that erp is nil and val is of the form (:STOP-LD . x), as is returned by default by ld upon an evaluation error. A key effect of this change is for the case that a .acl2 file 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.pl executes 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 ld above returns (mv nil (:STOP-LD 2) state). Because ld-error-action at 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-action is (: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).

New Features

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 IF. Thanks to Eric Smith for suggesting the development of such a feature, which can be useful in rewriting-based tools.

There is a new `make' target to build an ACL2 executable using save-exec. See save-exec, in particular the new discussion at the end of that topic. Thanks to Eric Smith for requesting such a utility.

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, :tc (translate and clean), has been added. It translates a given form and then ``cleans it up'', returning a logically equivalent but often simpler term in which logically irrelevant but operationally important tags have been removed. The variants :tca and :tcp use different degrees of ``cleaning.'' These are particularly useful for seeing the logical meanings of loop$ terms as well as terms involving mbe and return-last.

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 ACL2_PROJECTS; see project-dir-alist. By default, the project-dir-alist has only one entry, which associates the keyword :SYSTEM with the community-books directory, books/. The project-dir-alist generalizes the notion of system books directory, assigning meaning to the :dir argument of include-book and ld and to sysfile arguments of add-include-book-dir and add-include-book-dir!. Thanks to Sol Swords for requesting such a capability and for helpful design discussions. (Technical Note: Implementation-level changes are summarized in comments in the form (defxdoc note-8-6 ...) in community-book system/doc/acl2-doc.lisp.)

A new break-rewrite command, :pot-list, shows the list of the polynomials that are assumed in the current context. See brr-commands and see brr@. Thanks to Alessandro Coglio and Eric Smith for conversations leading to this enhancement.

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 from some DO loop$s. See stating-and-proving-lemmas-about-loop$s for a brief discussion.

A new :linear rule, acl2-count-car-cdr-linear, is now built into ACL2, as follows. Thanks to Eric Smith for suggesting this improvement (slightly renamed here) to what we originally added.

Theorem: acl2-count-car-cdr-linear

(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.

Lambda objects in positions of ilk :FN are now subjected to a size limitation. See explain-giant-lambda-object.

The keyword :off for the utility with-output (also with-output!) can take on a new value, :all!, which is treated exactly the same as using arguments :off :all :gag-mode nil.

The new utility with-cbd creates a scope for an indicated value of the connected book directory (see cbd). Calls of with-cbd are allowed in books as well as in encapsulate and progn events; see embedded-event-form. Thanks to Sol Swords for requesting that with-cbd be legal in embedded events.

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 .port files by the build system (see build::cert.pl).

The symbol, number, is now a legal type-spec.

It is now permitted for a stobj s to occur more than once as an actual parameter in a function call, provided each such occurrence is in a position where a stobj congruent to s is expected (possibly s itself). Thanks to Sol Swords for providing a relevant example, which appears in a comment in the definition of function stobjs-in-out in the ACL2 sources.

Heuristic and Efficiency Improvements

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.

Bug Fixes

Fixed a soundness bug based on rules of class :meta or :clause-processor that would be exported from an encapsulate event with a non-nil signature list. A proof of nil in Version_8.5 may be found in the community-books file, books/system/tests/transparent-functions-input.lsp; search for this paragraph there.

It was probably a soundness bug to allow a defaxiom event to designate a rule of class :meta or :clause-processor in its :rule-classes. That is no longer allowed; skip-proofs may be used instead if one believes that the proposed formula is a theorem.

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 (increment-file-clock state) after calling read-file-into-string. Formerly the error was avoided if the write-date of the file didn't change between the two reads, but the following example shows how this permitted two calls with identical arguments to produce different results, logically causing read-file-into-string to violate the axiom x = x.

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-Z and 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 state hasn't changed. (Probably the state hasn't changed; at any rate, the parts of the state relevant to read-file-into-string haven'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 bounded-integer-listp, which may have allowed illegal proof-builder commands to be attempted. Thanks to Grant Jurgensen for pointing out this bug.

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 defthm but not thm, but now it is the case for both. You can see the change for the following call, whose Rules summmary formerly included (:ELIM CAR-CDR-ELIM) but no longer does so.

(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 position-ac. Thanks to Eric Smith for pointing them out.

Fixed translation of DO loop$ expressions, so that the next-to-last argument of the resulting do$ call quotes the untranslated measure instead of the translated measure.

Several improvements were made to the FOR loop$ utility (also see for-loop$, to reflect more accurately the Common Lisp loop utility. This matters because in guard-verified code, loop$ becomes loop. Here are the most user-visible such changes.

Run-time guard-checking for loop$ operators SUM and APPEND did not include a check that the value produced at each iteration is a number or true list, respectively. That has been fixed so that, for example, the expression (loop$ for v in '(1 a 2) sum v) now causes a guard violation (because a is not a number), where previously it did not.
For a form (loop$ for tail on lst ...), the target term, lst, no longer needs to satisfy true-listp. For example, the form (loop$ for tail on '(a b . c) collect tail) no longer causes a @(see guard) violation.</li> <li>Run-time @(see guard)-checking for an expression @('(loop$ for tail on lst ...) now includes a check for the target, lst, that its final tail (i.e., , (last-cdr lst) satisfies the declared type of the corresponding iteration variable. For example, evaluation of the loop$ expression below now produces a guard violation as shown, but it formerly did not produce a guard violation.
```
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 lo and hi, the increment inc, and the last value tested, in expressions (loop$ for i from lo to hi by inc ...).

Fixed a low-level bug in source function translate-declaration-to-guard1-gen that was incorrectly creating untranslated terms in some cases from type declarations of the form (type (signed-byte _) _) or (type (unsigned-byte _) _). Here is an example of an event that is rejected without the bug fix.

(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 local wrapper could be ignored when writing the book's certificate.

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.

Warnings for repeating a goal name in the hints now appear even when the repetition is only up to case. For example, such a warning is generated now for :hints (("Goal" :use foo) ("GOAL" :use bar)) where formerly it was not. The discussion of this situation in documentation topic hints has been improved.
It was incorrectly documentated in topic hints, in the discussion of :do-not hints, that it is illegal to associate a goal name with the empty list of hints, as in ("Goal"). This behavior was actually allowed; an empty such hint was simply ignored. This continues to be allowed (for backward compatibility) but the documentation has been updated; also, these empty hints are now ignored for purposes of the warnings mentioned above (formerly they were considered when looking for repetition of goal names).

A bug in the brr commands :eval$, :go$, and :ok$ was fixed so they now behave as described in the documentation for 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-nil at that time. Thus, that situation no longer disqualifies such a world from supplying the portcullis commands to a book to be certified without keyword argument :skip-proofs-okp t of certify-book. Thanks to Sol Swords for pointing out this bug.

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)))))

Changes at the System Level

The `make' target, save-exec, now builds custom-saved_acl2 unconditionally. Thanks to Grant Jurgensen for pointing out (in GitHub Issue #1422) that there can be untracked implicit dependencies that make this necessary.

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 nil for the first return value of sys-call+ and sys-call*. Also, a bug has been fixed for sys-call+ in the case of GCL as the host Lisp. Thanks to Eric Smith for queries leading to these changes.

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.”

Start-here provides a guide for those getting started with ACL2.
Recursion-and-induction has been extensively modified from past, standalone versions by J Moore, and is now integrated with the rest of the documentation. Thanks to Vivek Ramanathan for helpful feedback.
Gentle-introduction-to-acl2-programming has also been updated from past standalone versions and integrated into the rest of the documentation.
Loop$-primer provides an extensive primer on the the ACL2 loop$ feature.

Allow ld output in raw-mode to go to other than the channel, *standard-co*. Thanks to Vivek Ramanathan and Warren Hunt for an example illustrating the issue.

EMACS Support

A set of tools for assisting in the conversion of certain HTML to xdoc may be found, without much documentation, in emacs/html-to-xdoc.el. Note that its release was approved by DARPA with “DISTRIBUTION STATEMENT A. Approved for public release. Distribution is unlimited.”

Experimental Versions

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).

Subtopics

Note-8-6-books: Release notes for the ACL2 Community Books for ACL2 8.6