Note-8-0
ACL2 Version 8.0 (December, 2017) 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 7.4 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-0-books for a summary of changes made to the ACL2 Community Books
since ACL2 7.4, including the build system. Also note that with each release,
some built-in functions that were formerly in :program mode are
now guard-verified :logic mode functions.
Changes to Existing Features
The macro, case-match, now treats keywords as constants when they
occur in patterns. For example, the following form evaluates to 3 where
formerly an error occurred:
(let ((x '(:foo 3)))
(case-match x
((:foo y) y)
(& 17)))
Thanks to Keshav Kini for suggesting this improvement.
Several changes have been made to sys-call and sys-call+,
and a new utility, sys-call*, has been added. These stem from
feedback from an observation by Eric Smith: sys-call could invoke the
operating system when simplifying terms (see sys-call for an example).
We thank Eric for helpful discussions. Changes include:
- When sys-call is invoked during a proof (from a prover call or
invocation of the proof-builder), it no longer can make a (potentially
dangerous) call to the operating system. If such an invocation occurs during
evaluation of a clause-processor or metafunction, an error will be
signaled.
- Sys-call+ continues to call the OS during proofs, but now it only
does so when applied to the actual ``live'' ACL2 state.
- A new utility, sys-call*, combines some features of sys-call and sys-call+; it takes state and takes effect even
during proofs like sys-call+, but like sys-call it does not capture
output. Thus, it can be a good choice in place of sys-call for
clause-processors and metafunctions, now that sys-call would cause an
error.
- The guards are no longer t. Now, the guard for all three functions
specifies the application of a string (the command) to a true list of
strings (the arguments).
- The executable-counterpart of sys-call is disabled by
default.
Several symbols have been added to the list *ACL2-exports*,
including LET (thanks to Eric Smith for that suggestion).
When a single-threaded object is being used where an ordinary object is
expected, the error message has been improved to show the enclosing form.
Moreover, such an error message can now appear when congruent stobjs are
involved, where formerly the error was blamed on the shape of the result.
Thanks to Sol Swords for bringing the latter problem to our attention with a
helpful example. (See a comment in ACL2 source function translate11-call
for a simplified version of that example.)
The banner printed when there is a raw Lisp error now points to a new documentation topic, raw-lisp-error. Thanks to Keshav Kini for most
recently pointing out that fmt can cause a raw Lisp error.
When suppressing output of all types other than error — see
set-inhibit-output-lst — then errors may be reported with
considerably less noise than before, because of the following changes. Thanks
to Eric Smith, Alessandro Coglio, and Stephen Westfold for helpful
discussions and feedback.
- When all output is inhibited except error output, the generic failure
message for events is suppressed for encapsulate, progn,
progn!, and make-event.
- When a call of make-event specifies keyword :on-behalf-of
with value :quiet or :quiet!, an error for make-event expansion
is generally suppressed; see make-event-details.
- A failed call of progn no longer prints "PROGN failed!";
similarly for progn!.
Some warnings have been made more compact for including uncertified books.
Thanks to Eric Smith for suggesting such an improvement.
The (minimal) support for infix printing has been removed. (See the Essay
on infix printing in ACL2 source file axioms.lisp for more information.)
However, as a result it is now possible to call certain functions during
evaluation of defconst forms, and during macroexpansion — in
general, during any evaluation when so-called ``safe mode'' is active and a
function with raw Lisp code is encountered. For example, the following form
was formerly rejected but is now accepted.
(defconst *c* (fms-to-string "abc~x0" (list (cons #\0 (expt 2 4)))))
Thanks to Eric Smith for suggesting such a change.
The role of ruler-extenders for redundancy of defun forms
has been simplified; see redundant-events. Thanks to Alessandro Coglio
for contributing a patch for this change. Moreover, there was a bug: the
redundancy check for definitions could allow the new definition to be
redundant even when it specified more than one value for
:ruler-extenders, which is illegal. This has been fixed. Thanks to
Alessandro Coglio for bringing this issue to our attention.
Modified the built-in rule complex-0 to one that is simpler but
equivalent, and modified the definition of conjugate so that it always
returns a number (essentially by ``fixing'' its argument). We thank Keshav
Kini for suggesting such changes, and for helpful discussions we also thank
Alessandro Coglio and Sol Swords, who suggested the definition of
conjugate that we ultimately installed.
The system-level utility, trans-eval, now prints a warning by default
when its call modifies a user-defined stobj. This feature can be
defeated but it may be best to allow the warning to be printed. See trans-eval and, especially, see user-stobjs-modified-warnings. A
related change is that in order to call ld in the body of a
definition, a new keyword argument, :ld-user-stobjs-modified-warning,
must be supplied. See ld. (Note: This issue was raised some time ago
by Sol Swords.)
Substantially improved error messages for illegal applications of theory functions enable, disable, set-difference-theories, union-theories, and intersection-theories.
Theory warnings have been enhanced to report enabling or disabling of the
definition rune for an undefined primitive like cons.
Thanks to Eric Smith for pointing out that ACL2 quietly lets one enable or
disable undefined primitives to no effect, and also for feedback leading to
improvements on the initial implementation of this change. For details, see
theories-and-primitives, specifically the last section, which pertains
to primitives.
Removed the symbol let-beta-reduce from the list
*initial-untouchable-fns* because let-beta-reduce is not a known
function symbol.
The :do-not-induct hint no longer accepts keyword arguments other than
:otf-flg-override and :otf, which would produce illegal theorem
names in the report of skipped goals. Thanks to Eric Smith for a query that
led us to clean this up.
Duplicate hypotheses have been eliminated for events generated by defabsstobj. Thanks to David Rager for bringing this issue to our attention
and for helpful conversations.
It is now legal for the bindings of a stobj-let form to call
accessors of a stobj, st1, on a stobj st2 that is congruent to
st1. See nested-stobjs. Thanks to Sol Swords for requesting and
explaining this feature, implementing it, and providing tests. To see tests,
search for ``how congruent stobjs may be used in stobj-let'' in community-book books/system/tests/nested-stobj-tests.lisp.
A low-level error starting with ``HARD ACL2 ERROR in
FIND-MAPPING-PAIRS-TAIL'' has been eliminated. This error could formerly
occur when using redefinition; see comments in ACL2 source function
find-mapping-pairs-tail1 for two simple examples. We thank Yan Peng for
bringing this issue to our attention. Note that although we make some effort
to support redefinition, we do not guarantee that it always works well; for a
relevant warning, see ld-redefinition-action.
Several related changes have been made in ``second-order''
capabilities.
- The function magic-ev-fncall could invoke functions that should
not be invoked because they require a trust tag (see defttag) or they
are untouchable (see push-untouchable). A check is now in place to
prevent this; see magic-ev-fncall. For example, evaluation of the form
(magic-ev-fncall 'sys-call '("pwd" nil) state t nil) no longer prints
the current directory; instead it results in an error.
- It was possible for system function ev-fncall-w to subvert such a
check by placing it under a program-wrapper; so ev-fncall-w is now
untouchable.
- A new function, ev-fncall-w!, always performs the check, and may be
used in place of ev-fncall-w. But consider instead using the documented
logic-mode function magic-ev-fncall.
- The first argument of magic-ev-fncall no longer needs to be in logic mode.
- Magic-ev-fncall can execute considerably more quickly than before;
thanks to Eric Smith for sending an example that helped us to implement this
improvement.
- Both oracle-apply and oracle-funcall have been eliminated. Use
magic-ev-fncall where you would otherwise use one of those.
Expressions in table events may now use not only the
variable, WORLD, but also the variable, ENS. See table.
New Features
A new utility, apply$, provides a weak version of the Common Lisp
second-order utility, apply. Using this new primitive the user can
define functions like map, which can apply certain function symbols and
lambda expressions.
Added utility checkpoint-summary-limit. Thanks to Mihir Mehta for
an email leading to this addition.
A new utility, set-register-invariant-risk, provides a way to avoid
inclusion of the invariant-risk check in code generated by ACL2 for
executable-counterpart functions (see evaluation). The effect of
set-register-invariant-risk is limited to the enclosing book or encapsulate event. Thanks to Eric Smith for a discussion leading to this
feature.
The new functions read-object-with-case and
print-object$-preserving-case are variants of read-object and
print-object$, respectively. The function read-object-with-case
lets you specify that case is preserved, inverted, or converted to lower case
or (as with read-object) to upper case. The function
print-object$-preserving-case prints symbols without escaping them for
case; for example, the symbol in the current package with name "abc" is
printed as abc, not as |abc| as would be printed by
print-object$. See io.
New macro with-output! is the same as with-output except for
two differences: with-output! can be called in code, but it does not
generate an event form.
Now complex-definition is a disabled rewrite rule (formerly rule-classes nil). Also added (enabled) rules default-pkg-imports,
default-code-char, and default-intern-in-package-of-symbol. All of
these may be found in ACL2 source file axioms.lisp. Thanks to Keshav
Kini for email that led us to add these rules.
New function get-enforce-redundancy queries the world on
whether redundancy is being enforced. Thanks to Eric Smith for requesting
this feature.
It is now possible to obtain output that is less likely to depend on the
directory where it was created, by evaluating the form (assign script-mode
t). (This capability supports the new tool, run-script.)
We added support for more detailed reports on the progress of
forward-chaining. However these reports are only available on an experimental
basis by redefining the system function forward-chain1 as directed by a
comment at the top of that defun. Users who find this level of reporting
useful are encouraged to tell us as we could incorporate it into the
documentation topic, forward-chaining-reports.
Normally, hard error messages (see er) are not inhibited. A new
state global, INHIBIT-ER-HARD, inhibits hard error messages when
ERROR output is inhibited; see set-inhibit-output-lst.
Heuristic and Efficiency Improvements
The checking done for invariant-risk has been relaxed, so that it no
longer causes any slowdown in calls of :logic-mode functions.
A low-level system function, cross-prod (which is used by tau-system), now uses tail-recursion, which may avoid some stack
overflows.
Forward-chaining was improved so that if a :forward-chaining
rule produces a conclusion that is a disjunction, the system watches for later
type-set information about the disjuncts. E.g., if we forward-chain to
(OR p q) and later in the same forward-chaining process q becomes
false, then p is made true. We thank Dave Greve for providing an example
requiring this.
An optimization for removing stobj recognizers, long applied to
bodies of executable definitions, is now also applied to guards.
Thanks to Sol Swords for suggesting this change and its implementation.
The function resize-list is now defined using mbe so that
its execution is tail-recursive. Thanks to Martin Simmons of LispWorks
Technical Support for diagnosing a stall in the certification of community
book books/centaur/truth/perm4.lisp as being due to a stack overflow
caused by an invocation of resize-list. Based on his advice we no longer
automatically grow the stack in LispWorks; this will ease debugging when
compilation is done with safety 3. The maximum stack size is 399998, at least
in our 64-bit LispWorks build.
Bug Fixes
Soundness bugs have been fixed in the handling of stobj-let, due to
aliasing that could take place by binding two different but congruent stobjs
to the same stobj. To see examples, search for ``soundness'' in community-book books/system/tests/nested-stobj-tests.lisp. We are very
grateful to Sol Swords not only for bringing this to our attention, but
especially for his contributions to a fix through helpful conversations and by
providing code and examples.
A bug in the proof-builder's command, rewrite (or equivalently,
r; see ACL2-pc::rewrite), avoided creating necessary subgoals,
which can presumably be unsound. That bad behavior could occur when the
third (and optional) argument of that command was a non-nil value other
than t.
The built-in evaluator functions for ACL2 relied on a system function,
ev-fncall-w, that was not a function! We do not see how to exploit this
oddity to prove nil, since ev-fncall-w is guaranteed never to be in
logic mode. However, it is clearly undesirable. In the following
example, the two ev-fncall-w calls gave different answers on the same
inputs — (mv nil 7) and (mv nil 12) — but now the second
call results in an error.
(defun foo (x y) (+ x y))
(assign old-w (w state))
(ev-fncall-w 'foo '(3 4) (@ old-w) nil nil nil t nil)
(u)
(defun foo (x y) (* x y))
(ev-fncall-w 'foo '(3 4) (@ old-w) nil nil nil t nil)
The check for the requisite theorems supporting a defabsstobj event
included a case where the check was too weak, and it also could cause an
unexpected assertion. The first of these could probably cause unsoundness.
Thanks to Sol Swords for finding these issues and providing fixes.
A small change in defstobj can lead to improved automation for some
guard proofs involving stobj-let. Thanks to Sol Swords for
sending an example, which guided us to add a test (as suggested by Eric
Smith) in community book system/tests/nested-stobj-formals.lisp.
Formatted printing (with fmt, cw, etc.) failed to respect
newlines encountered while processing ~s and ~S directives. This
has been fixed; see books/system/tests/fmt-to-string.lisp for examples
that behave well now but formerly did not. Thanks to Eric Smith for pointing
out this problem and sending, in essence, the following example.
(cw "~s0"
(string-append-lst
(make-list 100
:initial-element
(coerce '(#\A #\B #\C #\D #\E #\F
#\G #\H #\I #\J #\Newline)
'string))))
A bug that was in the tau-system is illustrated by the following
example sent by Grant Passmore, in which tau discovers that the function being
defined always returns nil, hence implies everything. Tau no longer
causes an error in this situation.
(defun f (x) (> x 0))
(defun g (x) (< x 0))
(defun h (x) (and (f x) (g x)))
Moreover, tau ``knows'' that the function h above is contradictory, as
evidenced by the successful proof of the thm below.
(thm
(implies (h x) (consp x))
:hints (("Goal" :in-theory '((:e tau-system)))))
Fixed a bug in :pe! that could result in an error in :pe!
:here when the most recent command is an encapsulate event.
It was possible to be in raw-mode, when including an uncertified book with
a call of progn! that first sets raw-mode set-raw-mode and
then causes a raw Lisp error. This has been fixed.
It is now possible to invoke verify-termination without an error
occurring due to the presence of untouchable variables or functions in the
definition (which hadn't prevented earlier admission in program mode).
Thanks To Eric Smith for bringing this issue to our attention.
ACL2 has supported, and continues to support, defun forms that
include the ACL2 state as an argument without declaring state
explicitly to be a stobj. This is done by first evaluating
(set-state-ok t). But in that case, the guard for such a function
erroneously failed to include (state-p state), which can have unfortunate
consequences; see books/system/tests/state-p-in-guard.lisp in the community-books. This has been fixed. Thanks to Alessandro Coglio for
contributing a fix and for helpful conversations.
Fixed bugs in reporting of errors and warnings by defchoose when
pertaining to ignored variables. Thanks to Eric Smith for bringing one of
these to our attention.
Fixed a bug in the proof-builder: hints on the prove
command were not being passed down to induction. Thanks to Mihir Mehta for
bringing this bug to our attention with a reproducible example.
Fixed a low-level bug (in source functions note-relieve-hyp-failure),
discovered by using the new community book
books/system/check-system-guards.lisp. That book, which is useful for
system development, checks all top-level calls of built-in functions that are
in logic mode, guard-verified.
Changes at the System Level
When building the combined manual, an error occurs if there is more than
the single expected broken link. Thanks to Alessandro Coglio for helpful
discussions. Notes. (1) This uses a new keyword argument available in
xdoc::save, :broken-links-limit. (2) There is no such limit for
saving the text-based manual.
As usual, several documentation improvements have been
made, for example, clarification made in the topic local-incompatibility thanks to Keshav Kini and Yan Peng. A new
documentation topic, evaluation, is probably long overdue: it
explains ACL2 evaluation with a focus on the notions of the
``executable-counterpart function'' (sometimes called the ``*1*
function'') and the ``submitted function'' (sometimes called the
``raw-Lisp function'').
Environment variable SBCL_USER_ARGS allows one to pass runtime-options
to calls of ACL2 built on SBCL, without having to call save-exec.
Thanks to Sol Swords for requesting this capability. Example:
(export SBCL_USER_ARGS="--lose-on-corruption" ; ./sbcl-saved_acl2)
There is a new documentation topic, talks, which has a link from the
ACL2 home page (with Applications, Tours, and Tutorials/Demos). Additional
contributions to this topic are welcomed!
For SBCL, the runtime option --disable-ldb is now supplied by the
saved_acl2 script, which avoids passing control to the
lowest-level (ldb) debugger (from which recovery is probably impossible).
Without this option, a parallel run of cert.pl (see build::cert.pl) can stall out when a single failure passes control to the
ldb debugger.
Some infinite loops are now avoided in the debugger for SBCL (and perhaps
some other Lisp implementations). Thanks to Keshav Kini for sending an
example and suggesting a fix, which we incorporated, as well as for helpful
conversations. Implementation note: the definition of constant
*our-standard-io* in ACL2 source file interface-raw.lisp explains
the issue.
Warnings were being produced by include-book in CCL, and perhaps
some other Lisps, when including a book that redefines a function as a macro
or vice-versa. We have eliminated those raw Lisp warnings.
It is now checked that the books/ directory exists before attempting
any operations using 'make' on that directory. Thanks to Keshav Kini for
suggesting this check, since there are source-only distributions, without the
books.
(SBCL only) The setting of environment variable SBCL_HOME has been
tweaked to be more robust. In particular, we expect it to be unnecessary, and
even inadvisable, to set SBCL_HOME manually. Thanks to Keshav Kini for
contributing this change.
(CMUCL only) ACL2 Version 8.0 cannot be reliably run on CMUCL, so we have
disabled building ACL2 on CMUCL. The CMUCL implementor is aware of the
problem, and we are hoping for a fix before the next ACL2 release
The state global variables, serialize-character-system and
serialize-character, are now preserved after make-event
expansion. This change for serialize-character-system allows the use of
make-event to avoid a stack overflow when writing out a certificate file; see set-serialize-character-system.
EMACS Support
Now, tags table TAGS-acl2-doc is automatically built when building the
manual unless environment variable TAGS_ACL2_DOC has value SKIP. It
can also be built by using the new event xdoc::save-rendered-event.
See ACL2-doc and see xdoc::save-rendered-event. Thanks to Eric
Smith and David Rager for discussions leading to this enhancement. That tags
table can also be built when building ACL2; see ACL2-doc.
Made miscellaneous fixes for ACL2-doc: added Shift-<tab>
(more precisely, <backtab> to do the same thing as
Control-<tab> (thanks to Eric McCarthy for the suggestion), avoided the
use of setf (not always defined without requiring the cl package),
avoided a potential error (when variable large-file-warning-threshold is
nil), and avoided an infinite loop on some platforms when quitting
acl2-doc.
Defined `meta-,' in emacs/emacs-acl2.el to be Emacs function
tags-loop-continue, which is how it has traditionally been defined by
Emacs but might be defined differently in some versions of Emacs 25 (and
perhaps later). NOTE: Put (setq *preserve-tags-loop-continue* t)
in your .emacs file before loading ACL2 file emacs/emacs-acl2.el, if
you want to avoid redefining `meta-,'. Thanks to Keshav Kini and Mihir
Mehta for helpful discussions.
Removed both non-ascii characters from emacs/emacs-acl2.el. Thanks to
Keshav Kini for the suggestion.
For documentation printed at the terminal with :doc, links
(enclosed in in square brackets, ``[..]'') continue to be printed with respect
to the "ACL2" package (that is, as though the current package were
"ACL2"). Now, however, where a link formerly might be printed as
``[acl2::foo]'', it is now printed as ``[foo]''; that is, a package prefix of
"ACL2" (regardless of case) is not printed.
Experimental Versions
Improved type-set reasoning for the function, imagpart.
Thanks to Keshav Kini for identifying the problem and suggesting a code
change, and for sending an example of a theorem that formerly failed to be
proved in ACL2(r).
Improved type-set reasoning for the function, complex.
Thanks to Keshav Kini for identifying the problem and sending a patch, which
we installed, together with examples of theorems that formerly failed to be
proved in ACL2(r) but now prove, in particular:
(thm (implies (and (real/rationalp a)
(not (rationalp a)))
(not (complex-rationalp (complex a b)))))
Since wormhole uses a lock (and has for some time), we modified
observation-cw so that it uses the same wormhole printing in ACL2(p)
(instead of using cw) that is used in regular ACL2. Thanks to David
Rager for a helpful discussion. If you see an increase in hangs while using
ACL2(p), please contact the implementors.
Fixed an infinite loop that could be caused with parallelism enabled when
there is an error, when Lisp variable *hard-error-is-error* has been set
to a non-nil value in raw Lisp (see hard-error).
Subtopics
- Note-8-0-books
- Release notes for the ACL2 Community Books for ACL2 8.0
