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.
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'' signature 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. 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.
The community-books file,
books/system/tests/transparent-functions-input.lsp has examples of the
use of transparent functions and related errors.
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.
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). At the moment the only
summary string used for inhibiting hard errors is "Call depth", for
rewriter stack overflows. On a related note, a new soft error summary string
is used for inhibiting soft errors, "Evaluation".
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.
Heuristic and Efficiency Improvements
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.
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.
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.”
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
Subtopics
- Note-8-6-books
- Release notes for the ACL2 Community Books for ACL2 8.6
