Note-8-1
ACL2 Version 8.1 (September, 2018) 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.0 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-1-books for a summary of changes made to the ACL2 Community Books
since ACL2 8.0, 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 evaluation of table guards now allows attachments. This is
important for the implementation of apply$ (see below).
A new keyword argument for defun-sk, :constrain, can specify
that the newly-introduced function is constrained rather than defined. See
defun-sk. Note that by constraining the function we make it possible
to attach to it, and also to introduce it as a guard-verified function.
We also made a minor change to defun-sk, by moving the call of extend-pe-table out of the generated encapsulate form.
(Of interest only to users of apply$.) When invoking defwarrant or defun$, a so-called `warrant' is introduced.
Warrants are now always guard-verified, with a guard of t.
Moreover, warrants are now executable in the top-level loop; for example,
after successfully processing (defwarrant foo) or (defun$ foo ...),
(warrant foo) will evaluate to t in the loop. (Note: each warrant
has an attachment, true-apply$-warrant, that always returns t; see
defattach.) Thanks to Dmitry Nadezhin for requesting these
enhancements.
It is now required to include the system book
projects/apply/apply-lemmas.lisp before evaluating a call of defun$
or defwarrant. This requirement, which is enforced with an error
that prints the necessary include-book form, avoids stack overflows
that could occur when that book is not included.
When performing make-event expansion under a surrounding local context, it is no longer illegal to set the ACL2-defaults-table. For example, the following event formerly caused an
error but is now legal.
(local (make-event (er-progn (set-ignore-ok t)
(defun foo (x) x)
(value `(value-triple ,(length (w state)))))))
Information printed when giving :use hints has been improved
for the case that a lemma-instance is a :termination-theorem or a :guard-theorem. Formerly, only the
name was shown in the `Hint-events' summary and in the proof
output; now, one will see ``names'' of the form (:termination-theorem
NAME) and (:guard-theorem NAME).
We improved redundancy checking for defun forms so that it is not
sensitive to whether state has a :stobjs declaration.
The warnings for weak type-prescription rules have been
eliminated. These warnings were issued when a rule was insufficient to prove
itself by type-set reasoning, but it seems more appropriate to
parse the formula into a type-prescription rule before applying that check
(for example, expanding away guard-holders, which was already done, and
beta reducing lambda applications, which was not). Then the chance of not
proving the result seems remote. Thanks to Keshav Kini for an example and a
conversation leading to this improvement.
The checksum computation that can support certifying or including
books — which is not used by default, but see book-hash
for how to enable it — has been improved. Specifically, at least one of
the community-books (namely, books/centaur/aignet/rwlib.lisp)
formerly caused a stack overflow (with host Lisp SBCL, at least) before making
this change. (Technical note: the change is to avoid memoization for calls of
fchecksum-obj with stack depth exceeding
10000.) Thanks to Keshav Kini for reporting
this issue and for related helpful communications.
When a break-rewrite command such as :eval or :go shows
that a rule fails because a backchain-limit is exceeded, more
information is printed than before. Now, the responsible rule(s) or global
backchain-limit is indicated. Thanks to Alessandro Coglio and Eric Smith for
requesting this enhancement.
The fancy string reader now accepts a string with three string quotes
followed by a closing curly brace. See fancy-string-reader, in
particular the final paragraph. Thanks to Sol Swords for contributing this
enhancement.
The ACL2 untranslate function, which converts the internal
representation of terms to user-level syntax, can now return calls of
mbe, mbt, ec-call, cw, time$, and
mv-let. Thanks to Alessandro Coglio, Eric Smith, and Stephen Westfold
for discussions leading to some of these changes. Such terms rarely occur in
practice because definitional bodies are stored with calls of guard-holders and cw expanded. However, here is an example of how they
could arise. First consider the following definition.
(defun g (n)
(declare (xargs :normalize nil))
(ec-call (natp n)))
Here is a log before the change.
ACL2 !>(verify (equal (g x) yyy))
->: 1
->: p
(G X)
->: x-dumb
->: p
(LET ((N X)) (EC-CALL1 NIL (NATP N)))
->:
After the change, the log instead ends as follows.
->: p
(LET ((N X)) (EC-CALL (NATP N)))
->:
It is now illegal by default to attach to built-in functions. To overcome
this default behavior, see defattach-system.
Improvements have been made to functions in the fmt family,
including for example fms, fmt-to-string, and cw.
(Also see discussion of fmx-cw under ``New Features,'' below.)
- Many guards have been strengthened, for example to imply that the
alist argument must satisfy character-alistp. Thanks to Eric
Smith for pointing out that an expression like (fmt-to-string "~x0" 3)
could cause a raw Lisp error (rather than causing a guard violation).
- Eliminated raw Lisp errors from ill-formed calls. Thanks to Jared Davis
for pointing out this problem in 2010 (!) with the example (cw "Bad:
~&0.~%" 5), and for Eric Smith for prodding us much more recently with the
example (cw "~&0" 'x).
- The utility fmx no longer prints an initial newline. Of course, a
call (fmx "<some-string>" ...) can be modified to generate an initial
newline (thus providing the former behavior) by adding the newline
tilde-directive, "~%", that is, (fmx "~%<some-string>"
...).
The previously-undocumented built-in-function, packn, now has a
slightly different behavior. Formerly, it always returned a symbol in the
"ACL2" package. Now, the package of the symbol returned is the package
of the first symbol in lst whose package is not "COMMON-LISP" if
any, else "ACL2". Thanks to Keshav Kini for suggesting this change and
providing its implementation.
The guard on apply$ (also the guard on apply$-lambda)
has been strengthened to require that a lambda be applied to the
correct number of arguments. The under-the-hood implementation for applying
lambdas has been made slightly more efficient as a result, though that
improvement may usually be trivial. Perhaps more important is that guard
verification may now catch bugs in the application of lambdas that were missed
previously.
The :dir argument to ld was previously ignored when the first
argument of the call of ld is not a string. Now, that is an error. If
you get this error, just remove the (previously ignored) :dir
argument.
The function magic-ev-fncall sometimes printed a message in the
error case in addition to returning that message. It now only returns that
message. Thanks to Sol Swords for bringing to our attention that
certification of a community book,
books/projects/x86isa/proofs/popcount/popcount.lisp, was printing a
warning about "Meta-level function Problem" for thousands of lines.
The definition of msgp has been strengthened to require that for a
cons pair, the cdr must satisfy character-alistp.
The proof-builder command, quiet!, now inhibits all output
except error output (and that too, if already inhibited).
Warnings have been modified that are labeled ``[Non-rec]'', generated for
rules with problematic occurrences of non-recursive function symbols. Now
they take into account rules of class :definition. Thanks to
Mihir Mehta for bringing this issue to our attention.
It is no longer required to specify :install-body nil in a definition rule when the function symbol is a member of the value of the
constant *definition-minimal-theory*. Thanks to Eric Smith for pointing
out that the utility, install-not-normalized, was failing on, for
example, eq. This change fixes that problem. Technical note for
system hackers only: Because of this change, the value of (body fn t
wrld) is no longer guaranteed to get the original definition of fn when
fn is in *definition-minimal-theory*; for that purpose use the new
utility, bbody.
Many error messages now show variables according to order of appearance,
where formerly the order was reversed. Thanks to Eric Smith for supplying an
example of a top-level form, + a b c, for which the error message
reported variables in reverse order: ``Global variables, such as C, B and A,
are not allowed.'' The message now says ``A, B, and C'' instead of ``C, B and
A.''
For value-triple, the keyword argument :on-skip-proofs
provides new behavior if it is given the value, :interactive. In that
case, evaluation is still done under a call of skip-proofs, as when
the value of :on-skip-proofs is t; but evaluation is skipped when
the reason proofs are being skipped is only that a book is being included or
the second pass is being made through an encapsulate. Thanks to Eric
Smith for requesting this feature.
Both fmt-to-comment-window and fmt-to-comment-window! have an
extra argument, print-base-radix, which is the same as the first argument
to the new utilities, cw-print-base-radix and cw-print-base-radix! (see below).
The undocumented constants *primitive-program-fns-with-raw-code*,
*primitive-logic-fns-with-raw-code*, and
*primitive-macros-with-raw-code* have been renamed respectively to
*initial-program-fns-with-raw-code*,
*initial-logic-fns-with-raw-code*, and
*initial-macros-with-raw-code*. Thanks to Alessandro Coglio for
suggesting these improved names.
The save-exec utility now utilizes a relative pathname in the
saved_acl2 script, which can allow it and a corresponding image file to
be moved, even across filesystems — though if there is an image file,
then probably the Lisp executable must have the same pathname even after the
move. Thanks to Eric Smith for suggesting this capability and providing a
hint for how to implement it, to Sol Swords for pointing out a limitation of
the initial implementation, and to this
website for making that solution robust.
The defevaluator macro, and more generally the notion of evaluator,
have been changed to include two new constraints inserted after
constraints 0 through 5. The new constraints are as follows, where <ev>
refers to the evaluator.
(IMPLIES (AND (NOT (CONSP X)) (NOT (SYMBOLP X)))
(EQUAL (<ev> X A) NIL))
(IMPLIES (AND (CONSP X) (NOT (CONSP (CAR X))) (NOT (SYMBOLP (CAR X))))
(EQUAL (<ev> X A) NIL))
These new constraints generated by defevaluator are named
<ev>-CONSTRAINT-6 and <ev>-CONSTRAINT-7
unless the keyword argument :namedp t is supplied,
in which case they are named <ev>-OF-NONSYMBOL-ATOM and
<ev>-OF-BAD-FNCALL. Thus by default (or if
:namedp is nil), this change increases by one the indices on
constraints for the specified function symbols, because they start at 8
instead of 6 — <ev>-CONSTRAINT-8, <ev>-CONSTRAINT-9, and so
on. Note that if you use functional instantiation to prove a theorem about
one evaluator given a theorem about another evaluator, you'll need to enable
the new rules (i.e., ev-constraint-6 and ev-constraint-7
or, if you use option :namedp t,
ev-of-nonsymbol-atom and ev-of-bad-fncall).
Thanks to Sol Swords for both suggesting and
implementing this extension.
Let-expressions are no longer eliminated from right-hand sides of
rewrite rules. See rewrite. This change improves efficiency of
the rewriter in some cases, by retaining subexpressions shared on the
right-hand side as the rewrite rule is applied. Thanks to Eric Smith for
requesting this change.
It was possible to declare a function symbol to be untouchable and
yet still execute it using apply$, thus violating the spirit of
untouchables. That is no longer allowed. Here is an example of such
execution that was formerly permitted, but is no longer.
(include-book "projects/apply/apply-lemmas" :dir :system)
(defun$ f (x) (declare (xargs :guard t)) (cons x x))
(push-untouchable f t)
(apply$ 'f '(3))
New Features
The summary now shows, by default, the list of doublets (f g)
for which f is a system function with attachment g (see defattach), when g differs from the initial attachment to f.
(Warning: The following describes advanced features that can likely be
ignored by most users. They are available using the new utility, defattach-system.) Three new system-level functions may be given
attachments: remove-trivial-equivalences-enabled-p,
assume-true-false-aggressive-p, and rewrite-if-avoid-swap. (Thanks
to Eric Smith for suggesting these, and to him and Alessandro Coglio for
helpful discussions.) By default, these have the attachments
constant-t-function-arity-0, constant-nil-function-arity-0, and
constant-nil-function-arity-0, respectively, which provide the existing
system behavior. But these attachments may be changed by the user.
- Remove-trivial-equivalences-enabled-p may receive the attachment
constant-nil-function-arity-0 to avoid the
remove-trivial-equivalences heuristic, which substitutes the equality (or
even equivalence) of a variable to a term into the rest of the
goal. (However, perhaps similar heuristics will still be used, for example as
part of the tau-system.)
- Assume-true-false-aggressive-p may receive the attachment
constant-t-function-arity-0 to strengthen the rewriter's use of the type-alist when diving into if terms. A common use is to rewrite what
amounts to (if (or test1 test2) (if test1 _ x) _); then the type-alist will note that test2 is true when rewriting x. This
change may slow down ACL2 considerably in some cases, and should rarely if
ever be necessary when calling the prover; but it can be useful in
applications that call the rewriter directly.
- Rewrite-if-avoid-swap may receive the attachment
constant-t-function-arity-0 to cause the rewriter — specifically,
source function rewrite-if — to avoid swapping true and false
branches of a call of IF, which could formerly happen when the test is a
call of NOT.
When the environment variable ACL2_CUSTOMIZATION_QUIET is set and not
"", there will generally be no output from ACL2 customization. A
special value of "all" for this variable will cause continued minimal
output after startup. See ACL2-customization.
New utilities, fmx-cw and fmx!-cw, are essentially the same
as cw and cw! (respectively), except that fmx-cw and
fmx!-cw are well-guarded, which can catch errors in the use of
tilde-directives. Thanks to Eric Smith for requesting such a capability. For
example:
ACL2 !>(fmx-cw "Hello ~s0." '(world))
ACL2 Error in TOP-LEVEL: Guard violation for FMX-CW-FN:
Illegal Fmt Syntax. The tilde-s directive at position 6 of the string
below is illegal because its variable evaluated to (WORLD), which is
not a symbol, a string, or a number.
"Hello ~s0."
ACL2 !>
New utilities, cw-print-base-radix and cw-print-base-radix!, are like cw and cw!, respectively,
except for an additional argument that specifies the print-base and,
optionally, the print-radix. Thanks to Eric Smith for requesting cw-print-base-radix.
A new event macro, set-in-theory-redundant-okp, allows in-theory events to be redundant, which prevents defund and
defthmd events from laying down command markers (as
seen, for example, using :pbt). Thanks to Eric Smith for asking
for a way for in-theory events to be redundant.
Heuristic and Efficiency Improvements
The implementation of wormholes has been tweaked to avoid an
efficiency problem. In the old implementation, an update to the wormhole
status was avoided in the case of equal old and new status values. That
update avoided some consing, but the equality test could be very slow; indeed,
:print-gv could be slow because of its use of wormholes. The new
wormhole implementation — specifically, the new raw Lisp implementation
of wormhole-eval — avoids that equality test, and also can avoid
consing by its use of destructive operations. That fixes one reason
:print-gv could be slow; a second change, made to the implementation of
:print-gv, is to pass nil as the wormhole-status (whs) argument
of make-wormhole-status. See make-wormhole-status for a
discussion of how that use of nil can avoid an expensive equality
test. Thanks to Alessandro Coglio and Eric Smith for sending an example that
illustrated the problem.
The following improvements have been made for evaluating calls of the form
(apply$ '(lambda ...) ...).
- An optimization had failed to be fully in place, causing such calls to run
slowly. That optimization compiles and caches ``tame compliant'' lambdas:
lambda forms whose guards are verified by the tau-system and
that are tame (see apply$). The optimization had been used in
the unadvertised use of ``The Rubric'' prior to the release of ACL2 Version
8.0. Warnings about non-tame-compliant lambdas will now appear when
appropriate, as had been the case in Version 7.4.
- The optimization above has been improved so that instead of three cache
lines, there is an efficient implementation using 1000 cache lines. That is
probably many more than are needed, but the large size is harmless. The
additional cache lines dramatically improve speed when more than three lambdas
are actively being applied; see community-books file
books/system/tests/apply-timings.lisp.
- ACL2 no longer causes an error when the cache is in an inconsistent
state; instead, the cache is suitably reset quietly.
Rewriting of calls of implies has been optimized in the cases that
the rewritten arguments are equal or at least one is a constant. Thanks to
Eric Smith for pointing out an incompleteness in the rewriting of implies
calls.
The algorithm has been tweaked for generating a type-prescription
rule to store for a given definition, so that the rule is sometimes stronger
than was previously the case.
Bug Fixes
There was a soundness bug in the automatic functional instantiation that
can be applied for a :termination-theorem lemma-instance. Thanks
to Eric Smith for sending an example to illustrate this bug, for suggesting
its cause, and for permission to include that example in a comment in the ACL2
sources definition of the constant, *non-instantiable-primitives*.
Bugs have been fixed in the tau-system that caused unsoundness
(going all the way back through Version 6.0, released December, 2012). The
problem was with conversion of a non-strict inequality with 0 to a strict
inequality when the quantity is known not to be 0; for example, (<= x 0)
was converted to (< x 0) when x was known to be non-zero. But of
course, this conversion is only valid when x is known to be a number.
Thanks to Yan Peng for sending an example that illustrates the bug, which in
its essence was the ability of ACL2 to prove this formula, which for example
is false when x = t: (or (< x 0) (= x 0) (> x 0)). If you encounter
a failure in a proof that formerly succeeded, the fix might be to add a call
of ACL2-numberp to the hypotheses of your theorem.
Fixed two bugs in apply$: we now disable the executable-counterpart of good-bye-fn to prevent quitting ACL2 entirely
during a proof, and we avoid the error ``ACL2 cannot ev the call of
non-executable function ANCESTORS-CHECK...'' by allowing attachments to be
used when checking table guards (as discussed above). Thanks to Dmitry
Nadezhin for sending replayable examples that exhibited these bugs.
Fixed guards for functions enabled-runep, enabled-numep, disabledp-fn, and disabledp-fn-lst, thus eliminating
bogus guard violations. Thanks to Alessandro Coglio and Eric Smith for
sending an example that illustrated the bug for enabled-runep. Technical
note: this fix was made by replacing calls of bounded-nat-alistp (which
is no longer defined) by calls of nat-alistp (which is newly defined).
We also made a corresponding tweak to the definition of
enabled-numep.
Warnings labeled with ``Double-rewrite'' failed to take into account
patterned congruence rules. This has been fixed. Thanks to Mihir
Mehta for pointing out the problem with a helpful example.
It is now possible, once again, to monitor rules of class
:linear. This capability has (accidentally) been unavailable
since Version 7.4. Thanks to Dmitry Nadezhin for reporting the bug with a
helpful example.
It was possible for users to change the attachments to built-in functions
badge-userfn and apply$-userfn, which support the implementation of
apply$. This is now prevented.
For defequiv, a :doc keyword argument was allegedly (in the
documentation) supported but caused an ugly error. The :doc keyword
argument is now fully eliminated. Thanks to Eric Smith for pointing out this
issue.
Fixed :pso and related utilities :pso!,
:psof, and :psog, to avoid printing some error
messages. Thanks to Keshav Kini for sending us an example to bring this bug
to our attention. Also tweaked these utilities to avoid accumulating later
event failure messages into the saved output for a previous proof attempt, and
to avoid some bogus output when invoked before the first proof attempt of the
session.
When an invocation of defthmd resulted in a macroexpansion error,
the failure did not cause an error message to be printed. This has been
fixed. Related tweaks improve error reporting, including a clearer error
message when attempting to supply :rule-classes nil with defthmd.
Thanks to Keshav Kini for reporting these issues.
When defattach was provided the argument :skip-checks nil, a
hard error was signaled. This has been fixed.
The case-match macro did not properly handle the !sym
construct when the symbol, !sym, is not in the "ACL2" package.
This has been fixed. Thanks to Alessandro Coglio for reporting this bug.
Fixed handling of some guard violation error messages for built-in
functions. For example, the form (apply$-lambda 3 nil) produces a guard
violation, but before this fix, the error message reported an implementation
error.
Fixed the :puff command to avoid certain errors involving
local events.
Redundancy notes could be seen during include-book while loading
the compiled file for a book. These notes (along with, perhaps, some other
output) have been eliminated. Thanks to Eric Smith for pointing us to this
problem with a reproducible example.
We eliminated an obscure hard error mentioning the source function
assume-true-false-if, which could occur in the middle of a proof. Thanks
to Dave Greve for pointing out this problem by sending us an illustrative
example that we could run.
It was possible to get a raw Lisp error from ill-formed calls of ec-call not intended for execution, for example, (defun foo (x) (non-exec
(ec-call x))). This has been fixed.
Certain syntactic requirements are normally applied to function bodies but
not to theorems. However, these were being applied under calls of flet. Consider the following example.
(thm
(flet ((foo (x) (car x)))
(foo (mv-nth 1 (mv x x)))))
This was rejected with an error: ``The expected number of return values for
(MV X X) is 1 but the actual number of return values is 2.'' This has been
fixed. Thanks to Eric Smith for bringing this problem to our attention.
A bug has been fixed in the logical definition of the function,
read-file-into-string2, which supports the macro, read-file-into-string. Thanks to Keshav Kini for finding this bug and to
Mihir Mehta for a query leading to Keshav's investigation.
The previous release was supposed to include a new utility, checkpoint-summary-limit, but that was missing. Thanks to Keshav Kini for
pointing this out (and supplying the expected implementation).
Fixed a bug in the guard for built-in function warning1-cw, which
could be seen for example by evaluating the form (warning$-cw 'my-ctx
"The :REWRITE rule ~x0 loops forever." 'foo). Thanks to Keshav Kini for
bringing this issue to our attention.
The definitions of the macros logand, logior, logxor, and logeqv were such that when any of these was applied to a
single argument, the expansion was simply that argument. For example,
(logand (foo a)) expanded to (foo a). These definitions failed to
reflect the fact that in Common Lisp, an error may be signaled if that single
argument does not evaluate to an integer. For example, the following
definition was admitted: (defun f (x) (declare (xargs :guard t)) (logand
x)); yet a raw Lisp error was signaled when attempting to evaluate (f
'x), in ACL2 built on Allegro Common Lisp. This bug has been fixed: now,
when any of these four macros is applied to a single argument, a, the
expansion is (the integer a). Thanks to Eric Smith for bringing this bug
to our attention.
Fixed :args to avoid hard ACL2 error when applied to IF
and to provide a clearer error message for Common Lisp functions not in ACL2.
Thanks to Eric McCarthy for sending examples to point out these issues.
A bug has been fixed that could cause an error when processing a legal
flet form, because the processing of a binding could interfere
inappropriately with the processing of a subsequent binding, as in the
following example.
(defun f (x) x)
(flet ((f (x) (cons x x))
(g (x) (f x))) ; processed with bad binding of stobjs-out for f
(g 3))
Fixed an error message saying that ``It is illegal for supporters of
DEFAXIOM events to receive attachments'' that failed during printing. Thanks
to Nathan Guermond for sending an example to point out this bug.
Changes at the System Level
Fixed the use of `<a href='URL'>...</a>' so that if URL has the
ampersand character in it, all will be well for both the web-based manual and
text-based rendering (as when :doc is used at the terminal or
ACL2-doc is used) provided that character is written as & in
the documentation string. Previously, the web-based manual could fail to
display the page for & in the documentation string, while with &
used, the web-based manual could display the page but the text-based rendering
showed & instead of simply &. Thanks to Cuong Chau for pointing
out that the topic double-rewrite was not being displayed in the
online manual (back when & was used in the URL in the documentation
string).
The "clean" target of "make" has been deprecated since ACL2 Version
7.4 (released in March, 2017). Its replacement is target "clean-lite"; or,
use target "clean-all" (or equivalently, "distclean") if you want a more
thorough cleaning.
(SBCL only) ACL2 has been updated so that it builds on recent SBCL
versions. In particular, the build was broken for SBCL 1.4.7, as SBCL changed
the ``RDTSC'' timing capability used in memoization. Thanks to Keshav
Kini for help with this issue, which has been resolved in ACL2 source file
memoize-raw.lisp, as explained in the comment there about
``read-cycle-counter''.
(CCL only) Raw Lisp error messages now mention the caller. Thanks to Eric
Smith for pointing out that this information wasn't being provided in the ACL2
loop even though it was being provided in raw Lisp.
EMACS Support
Removed setting of the buffer coding system from emacs/emacs-acl2.el.
Thanks to Keshav Kini for suggesting this change. This should avoid certain
modifications of ``unusual'' characters when saving a file.
Experimental Versions
The utility with-local-state no longer causes an error in ACL2(p)
with parallel-execution enabled. Thus, neither do fmt-to-string and related utilities, which call with-local-state.
Subtopics
- Note-8-1-books
- Release notes for the ACL2 Community Books for ACL2 8.1
