NOTE-6-0

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:

LICENSE change

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

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 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

Functions read-acl2-oracle and 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.

The function butlast now behaves more reasonably on arguments violating its guard. For example, (butlast '(1 2 3) -1) is now provably equal to (1 2 3) instead of to (1 2 3 nil). Thanks to Jared Davis for suggesting a change to the definition of butlast.

The utilities mfc-ts and 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 -- mfc-rw, mfc-rw+, and mfc-relieve-hyp -- are now macros that take (optional) keyword arguments :forcep and :ttreep. The :forcep argument is :same by default, providing the forcing behavior inherited from the environment (as described above); but it can be the symbol t or 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. See extended-metafunctions.

Many improvements have been made to the tau-system (see tau-system), including support for arithmetic intervals bounded by constants. Thus, for example, (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.

The 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!

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 (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 macro-aliases-table.

When :pe is applied to a built-in function that does not have a defining event, such as symbolp, :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.

The macros memoize and 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 removes 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.

NEW FEATURES

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 :logic 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 http://www.cs.utexas.edu/users/moore/acl2/open-architecture/. The 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 book, books/clause-processors/meta-extract-user.lisp, that extends the power of meta-extract hypotheses.

New utilities oracle-funcall, oracle-apply, and 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 (:induction binary-append). See theories. Thanks to Jared Davis for a useful discussion leading to this enhancement.

Defabsstobj events now take an optional :congruent-to keyword 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 inline and notinline declarations. Thanks to Jared Davis for requesting this feature.

The utility 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 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 :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.

HEURISTIC IMPROVEMENTS

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 :brr t is 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.

BUG FIXES

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 nil, which we include as a comment in source file ld.lisp, in (deflabel note-6-0 ...). We also thank Sol for helpful discussions about guards of functions introduced by 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 introduced for defabsstobj exports, along with a new top-level defabsstobj keyword, :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 set-absstobj-debug.

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 result of (mv erp val state) was sometimes treated as an error triple even when val is a stobj. Now, (mv erp val state) is an error triple only when erp and val are ordinary (non-stobj) values. Thanks to Warren Hunt and Marijn Heule for bringing this problem to our attention.

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 REPLACED-ST.)

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.

Fixed a bug in the guards to system functions fmt-char and fmt-var, which are no longer :logic-mode, guard-verified functions.

(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 community book books/misc/wet.lisp).

A directory, 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 books/interface/. Subdirectory emacs/ of that interface directory provides Emacs support for proof-trees as well an acl2-mode. This change has been reflected in ACL2 file 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 Perl), include 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 ACL2 environment 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 of *sbcl-dynamic-space-size*).

EMACS SUPPORT

EXPERIMENTAL/ALTERNATE VERSIONS

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-sk now 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.

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-theory hint 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.