ACL2 Version 6.0 (December, 2012) 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
CHANGES TO EXISTING FEATURES
Function 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
(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 `
; 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
The function butlast now behaves more reasonably on arguments
violating its guard. For example,
Many improvements have been made to the tau-system (see tau-system),
including support for arithmetic intervals bounded by constants. Thus, for
The defthm events printed by defabsstobj, namely
those that remain to be proved, are now given with
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!
The utilities defun-inline, defun-notinline, defund-inline, and 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.
The events add-invisible-fns and remove-invisible-fns now convert arguments as appropriate using the macro-aliases-table. For example, the event
Terms are now parsed into
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
Among the new features for system hackers are analogues of system function
More built-in functions are now guard-verified (and in
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
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
Defabsstobj events now take an optional
Flet may now include
Added definitions of functions nat-listp and ACL2-number-listp. 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
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
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 guards that
violated single-threadedness restrictions. Thanks to Sol Swords for bringing
this bug to our attention and supplying a proof of
Fixed a soundness bug in defabsstobj based on interrupted updates
of abstract stobjs. As part of the fix a new keyword,
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-triple) had been
implemented ambiguously, with the result that for a stobj,
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
Some possible error messages for defabsstobj have been fixed that had been ill-formed. Thanks to Sol Swords for bringing this bug to our attention.
Fixed a bug that sometimes caused the times displayed in the summary for certify-book to be smaller than the actual times.
(GCL only) Fixed a bug present in Gnu Common Lisp for
CHANGES AT THE SYSTEM LEVEL
The state global variable
Fixed a bug in the implementation of wet (which is actually in the
The community books file
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
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
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.
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.
Macros with-fast-alist, with-stolen-alist, and fast-alist-free-on-exit are 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.