Major Section: RELEASE-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 since Version 5.0 into the following categories of changes: existing features, new features, heuristic 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. But we start with one major change that is outside the usual categories:
The ACL2 license has been changed from GPL Version 2 to a 3-clause BSD
license, found in the
LICENSE file distributed with ACL2.
CHANGES TO EXISTING FEATURES
fmt-to-string and similar functions (see printing-to-strings)
now use the default right margin settings; formerly the right margin had been
set at 10,000. If you want the former behavior, you can use the
:fmt-control-alist, as illustrated below.
(fmt-to-string "~x0" (list (cons #\0 (make-list 30))) :fmt-control-alist `((fmt-soft-right-margin . 10000) (fmt-hard-right-margin . 10000)))
The use of attachments (see defattach) has been made more efficient,
avoiding some low-level checks (Common Lisp `
boundp' checks). Thanks to
Shilpi Goel for constructing an example that we used to help direct us to
remove inefficiency. The following results for that example -- a Fibonacci
program run on a machine interpreter in raw-mode (see set-raw-mode) --
give a sense of the potential speedup, though we note that a full ACL2(h)
regression showed no significant speedup.
; Time before the change: ; 0.89 seconds realtime, 0.90 seconds runtime ; Time after the change: ; 0.75 seconds realtime, 0.75 seconds runtime ; Time when cheating to avoid the cost of attachments, by redefining a ; function to BE its attachment (so, this gives a lower bound on possible ; execution time): ; 0.72 seconds realtime, 0.72 seconds runtime
read-acl2-oracle@par are no longer
untouchable (see remove-untouchable). We reported this change for
Version_5.0 but it was not made; thanks to Jared Davis for bringing this to
our attention. Function
get-timer also is no longer untouchable.
butlast now behaves more reasonably on arguments violating
its guard. For example,
(butlast '(1 2 3) -1) is now provably equal
(1 2 3) instead of to
(1 2 3 nil). Thanks to Jared Davis for
suggesting a change to the definition of
mfc-ap (see extended-metafunctions)
formerly never used forcing (see force). Now, by default, forcing is
allowed during execution of these functions if and only if it is permitted in
the rewriting environment where they are called. Moreover, these and the
mfc-xx utilities --
-- are now macros that take (optional) keyword arguments
:forcep argument is
:same by default, providing the
forcing behavior inherited from the environment (as described above); but it
can be the symbol
nil, indicating that forcing is to be enabled
or disabled, respectively. The
:ttree argument is
nil by default,
but when it is
t, then a second value is returned, which is a tag-tree.
Many improvements have been made to the tau-system (see tau-system),
including support for arithmetic intervals bounded by constants. Thus, for
(and (<= 0 x) (<= x 15)) is a tau predicate. The
documentation has also been improved
(see introduction-to-the-tau-system). Also see time-tracker-tau for
discussion of how the new
time-tracker utility can help discover ways
to detect slowdown related to the tau-system.
defthm events printed by
defabsstobj, namely those that
remain to be proved, are now given with
:rule-classes nil since there is
probably no intention to use them as rules. Thanks to Robert Krug for
suggesting that we consider this change.
The formal parameters for a macro definition (see defmacro) may now include
state and user-defined
stobjs. (However, macro formals may not
be declared as stobjs; see xargs.) Thanks to Jose Luis Ruiz-Reina for
raising this issue and to Rob Sumners for helpful conversations -- both of
these nearly 10 years ago!
defund-notinline have been simplified, by taking advantage of the
lifting of restrictions on formal parameters of macro definitions mentioned
above (involving symbols that happen to be stobj names). Now, when any
of the above four utilities is called with a given set of formal parameters,
those formals will be used not only for the generated
defun event but
also for the generated
defmacro event. (Previously, they had been
renamed for the
defmacro event in order to respect the stobj name
restriction that no longer exists.) Thanks to Jared Davis for pointing out
the value of making this change.
convert arguments as appropriate using the
example, the event
(add-invisible-fns append car) is now legal (though
probably not a good idea), because
add-invisible-fns is now sensitive
to the fact that
append maps to
binary-append in the
pe is applied to a built-in function that does not have a
defining event, such as
:pe now gives more useful output
that points to the documentation instead of printing a call of
ENTER-BOOT-STRAP-MODE. Thanks to Anthony Knape for bringing this issue
to our attention.
unmemoize now cause a warning rather than
an error in ACL2 (and work as before in ACL2(h)).
Terms are now parsed into
type-prescription rules in a manner that
let bindings both at the top level and in the conclusion (but
still not in the hypotheses of the rule). See type-prescription. Thanks to
Jared Davis for requesting such an enhancement.
Printing of numbers is now appropriately sensitive to the print radix; see set-print-radix. Thanks to Shilpi Goel for requesting this enhancement.
The system function
explode-atom no longer includes the radix indicator.
The new function
explode-atom+ may be used for that purpose.
Among the new features for system hackers are analogues of system function
simple-translate-and-eval that do not return
state. (Thanks to
David Rager for requesting this feature and helpful conversations on its
implementation.) This and other low-level changes are typically documented
in comments in the corresponding release note event, which in this case is
(deflabel note-6-0 ...).
More built-in functions are now guard-verified (and in
mode). Furthermore, a mechanism exists for marking yet more built-in
functions as guard-verified based on books contributed by users; see
Part II of
current state of that enterprise may be viewed by evaluating the constant
*system-verify-guards-alist*, which associates a community book name with
a list of functions. When ACL2 is built in the normal way, each of those
functions is marked as guard-verified when ACL2 is started up; but a special
developer build can be used to check that the indicated book, together with
its sub-books, proves that those functions are guard-verified.
Metatheorems (see meta) may now have additional hypotheses, called
``meta-extract hypotheses'', that allow metafunctions to depend on the
validity of certain terms extracted from the context or the logical
world. See meta-extract. Thanks to Sol Swords for providing an initial
implementation, together with very helpful discussions as well as a community
books/clause-processors/meta-extract-user.lisp, that extends the
power of meta-extract hypotheses.
oracle-apply-raw call a function argument on specified arguments.
Thanks to Jared Davis for requesting this utility.
A new utility makes it convenient to track time spent inside specified function calls or, more generally, during specified evaluation. See time-tracker.
New runic designators make it easy to refer to macro names when building
theories. Thus, for example, the object
(:i append) may be used in
theory expressions to designate the rune
See theories. Thanks to Jared Davis for a useful discussion leading to this
Defabsstobj events now take an optional
argument, much like
defstobj. Thanks to Sol Swords for requesting this
feature and for suggesting a very nice optimization that avoids the need to
prove additional lemmas.
Flet may now include
notinline declarations. Thanks
to Jared Davis for requesting this feature.
gc-verbose controls printing of messages by the garbage
collector, for certain host Lisps. See gc-verbose. Thanks to Shilpi Goel
for requesting this utility.
Added definitions of functions
Thanks to Harsh Raju Chamarthi for requesting these additions. Many
community books had varying definitions of these functions; these additions
guarantee that all books must agree on how these two functions are
defined. (Some community books have been changed in order that they remain
certifiable, given these additions.) Note that a few built-in
forward-chaining rules were modified in order to accommodate these
additions, and the definition of
integer-listp was modified to call
eq instead of
equal, like the other such definitions.
See get-command-sequence for a new utility that returns a list of commands between two given command descriptors.
We obtained a substantial speedup -- 13% observed for the regression suite,
and 8% observed for the ACL2(h) regression suite -- by tweaking the
break-rewrite implementation to eliminate virtually all of its overhead
when it is not in use (the default, which holds until
evaluated). Thanks to David Rager for a conversation involving ACL2(p)
performance statistics that suggested looking at changing break-rewrite
to boost performance.
The heuristics for automatically expanding recursive function calls have been changed during proofs by induction. Now, during induction, more terms that suggested the induction scheme are automatically expanded. Thanks to David Rager for providing an example and having discussions with us that spurred us to develop this heuristic improvement.
Fixed a soundness bug in
defabsstobj based on
violated single-threadedness restrictions. Thanks to Sol Swords for bringing
this bug to our attention and supplying a proof of
nil, which we include
as a comment in source file
(deflabel note-6-0 ...). We
also thank Sol for helpful discussions about guards of functions
defabsstobj, which has led us to enhance the
documentation; see defabsstobj.
Fixed a soundness bug in
defabsstobj based on interrupted updates of
abstract stobjs. As part of the fix a new keyword,
:PROTECT, has been
defabsstobj exports, along with a new top-level
:PROTECT-DEFAULT; see defabsstobj. We do some
analysis that we expect will avoid the use of
:PROTECT in many cases,
which is fortunate since the use of
:PROTECT t may cause a slight
slowdown in (abstract) stobj updates. Thanks to Sol Swords for bringing this
bug to our attention and supplying a proof of
nil, which we include as a
comment in source file
other-events.lisp, in the definition of function
Fixed a raw Lisp error that occurred when tracing a stobj resize function, thanks to an error report from Warren Hunt, Marijn Heule, and Nathan Wetzler.
Fixed a raw Lisp error that occurred for certain ill-formed signatures, as in the following example.
ACL2 !>(encapsulate (((f (*) => * :guard t))) (local (defun f (x) (consp x)))) *********************************************** ************ ABORTING from raw Lisp *********** Error: value (F (*) => * :GUARD T) is not of the expected type SYMBOL. ***********************************************
The notion of ``error triple'' (see error-triples) had been implemented
ambiguously, with the result that for a stobj,
st, the result of
evaluating the following two forms was the same:
(mv nil st state) and
(mv t st state). Of course, these are just examples; in general, a
(mv erp val state) was sometimes treated as an error triple
val is a stobj. Now,
(mv erp val state) is an error
triple only when
val are ordinary (non-stobj) values.
Thanks to Warren Hunt and Marijn Heule for bringing this problem to our
The ``with-error-trace'' utility,
wet, now works in the non-error case
when given a form that returns multiple values. (Note however that
STATE will be printed as
REPLACED-STATE; and similarly, a
user-defined stobj, say
ST, will be printed as
Some possible error messages for
defabsstobj have been fixed that had
been ill-formed. Thanks to Sol Swords for bringing this bug to our
Fixed a bug that sometimes caused the times displayed in the summary for
certify-book to be smaller than the actual times.
Fixed a bug in the guards to system functions
fmt-var, which are no longer
(GCL only) Fixed a bug present in Gnu Common Lisp for
#u (see sharp-u-reader).
CHANGES AT THE SYSTEM LEVEL
The state global variable
'distributed-books-dir has been renamed
'system-books-dir. On a related note, the documentation now refers
to ``community books'' rather than ``distributed books'', and there is a
corresponding new documentation topic; see community-books.
Fixed a bug in the implementation of
wet (which is actually in the
interface/, is no longer part of the ACL2 distribution.
Rather, it is a subdirectory of the ACL2 community books. Thus, if you fetch
those books in the usual way (see the installation instructions on the ACL2
home page), you will find a directory
emacs/ of that
interface directory provides Emacs support for
proof-trees as well an
acl2-mode. This change has been reflected in
emacs/emacs-acl2.el, so users will probably not be impacted if
they load that file into Emacs.
The community books file
books/Makefile-generic now causes, by default, a
backtrace to be printed when there is a raw Lisp error.
Some changes have been made to how regressions are run, i.e., to how the
community books are certified. (1) The standard regression now includes
community books directory
books/centaur. To skip these (for example, a
Windows system has encountered difficulty with them even after installing
ACL2_CENTAUR=skip with your `make' command. (2) A new
`make' (or environment) variable,
ACL2_JOBS, specifies the number of
parallel jobs to run, serving as a replacement for the
-j argument of
`make' that works for all community books, including those under directory
centaur; see books-certification-classic. (3) It is no longer necessary
to do an ACL2(h) regression in order to build a copy of the documentation
generated by Jared Davis's xdoc utility at
books/xdoc-impl/manual/preview.html; a vanilla ACL2 regression will build
this manual. (4) It is no longer necessary to set the
variable for ACL2(h) regressions if you want to use the executable
saved_acl2h in the ACL2 sources directory.
The ACL2 home page now has a search utility for documentation and books. Thanks to Shilpi Goel and David Rager for feedback on a preliminary version of this utility.
(only for SBCL with 64-bit ACL2(h)) The value of SBCL command line option
--dynamic-space-size for ACL2(h) on 64-bit platforms has been increased
from 2000 to 16000 (as explained in a comment in the ACL2 source definition
Among the enhancements for ACL2(r) (see real) are the following.
Thanks to Ruben Gamboa for his helpful role in making the following improvements made with Ruben Gamboa in support for non-standard analysis in ACL2(r).
Constrained functions can now be introduce as non-classical. See signature.
Defun-sknow takes a new keyword argument,
:CLASSICALP, that determines whether or not the named function is classical. See defun-sk.
Incorporated a bug fix from Ruben Gamboa for
ceiling. The default (for `bad' arguments) had been 1, but now we follow normal ACL2 practice by returning 0 in that case.
Among the enhancements for the HONS extension (see hons-and-memoization) are the following.
fast-alist-free-on-exitare now defined in ACL2(h), rather than being defined in the community book
"books/centaur/misc/hons-extra.lisp". Thanks to Jared Davis and Sol Swords for donating this code, and thanks to Jared for helpful discussions leading to this change.
Among the enhancements for ACL2(p) (see parallelism) are the following. We thank David Rager for his work in developing ACL2(p) and for his helpful role in these improvements.
A bug has been fixed that could leave one in a wormhole, awaiting input, after an error, such as an error in an
:in-theoryhint during a proof. Thanks to Shilpi Goel for bringing this bug to our attention.
A key checkpoint for a given goal is now printed only once. Previously, if a key checkpoint led to more than one goal pushed for proof by induction, the key checkpoint would be printed once for each such goal during the proof, and also once for each such goal in the summary at the end.