		Search-engine friendly clone of the ACL2 documentation.

Release-notes

Note-7-1

ACL2 Version 7.1 (May, 2015) 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.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.

The default build is hons-enabled, as for the previous release; but the generated executable is now saved_acl2, as discussed below. Please note that ACL2(c) (``classic ACL2'', i.e., ACL2 that is not hons-enabled) now builds as saved_acl2c, is deprecated, and will likely be unsupported or even eliminated in future releases.

See also note-7-1-books for a summary of changes made to the ACL2 Community Books since ACL2 7.0, including the build system.

Changes to Existing Features

For both add-include-book-dir and add-include-book-dir!, the second argument is no longer evaluated (which we think could perhaps have been exploited to get unsound behavior, by arranging for the value of the second argument to depend on state). Moreover, that argument can not only be a string, but also can be a sysfile: an object (:system . filename), where filename is a file name. When filename is a relative pathname, the meaning of such an object is the file with that pathname under the system books directory.

The event summary had not been printed when a proof is interrupted (that is, with Control-C). Now, summary information is printed for two summary types (see for example set-inhibited-summary-types): rules and hint-events.

By default, (memsum) is now truncated to 100 entries rather than to 20 entries. (Implementation note: raw Lisp variable *memoize-summary-limit* is 100 instead of 20.)

Calls of THE no longer cause a guard violation when guard-checking is nil. Also see the and see set-guard-checking.

Type declarations for let and mv-let forms are now guard-checked. Consider for example the definition: (defun foo () (let ((x t)) (declare (type integer x)) x)). Previously, evaluation of the call (foo) had failed to result in a guard violation error; now, it does, provided guard-checking is on (i.e., not nil or :none; see set-guard-checking).

The symbols ctx, hist, pspv, unquote, and value have been added to *ACL2-exports*. Thanks to Jared Davis for suggesting these additions.

Consider :use or :by hints in which a variable bound using the :instance keyword is in the wrong package. For example, for the hint :use ((:instance foo (x 3))), suppose that the lemma foo mentions the variable bar::x, but not x. This situation formerly caused an error, but now, x indicates the variable bar::x from the lemma foo. See lemma-instance, in particular Condition (4), which has been updated accordingly. Thanks to David Rager for a remark that led us to implement this enhancement.

The ld special ld-error-action may now have a value (:exit N), where N is a natural number. If an error occurs for a call of ld, then this value causes the ACL2 process to quit with exit status N. See ld-error-action. Note that ld-error-action is set to this new value when using the cert.pl utility provided with the community books; see build::pre-certify-book-commands. Thanks to David Rager for presenting an example showing how this change can make it easier to locate certain certification failures, and thanks to Sol Swords for helping in the design of this enhancement.

A "Theory" warning is still printed when definitions of certain built-in functions, such as mv-nth, are disabled; similarly for some built-in executable-counterpart rules. However, we now print such warnings only when the disabling occurs, rather than every time an in-theory event or hint is evaluated. For example, if you evaluate (in-theory (disable mv-nth)) followed by (in-theory (disable append)), then the second event will no longer produce a warning about mv-nth. Thanks to Eric Smith for (most recently) suggesting such a change.

(SBCL only) ACL2 built on SBCL now reports bytes usage, both in time$ and in memsum, essentially exactly as has already been done for ACL2 built on CCL. Thanks to Jared Davis for suggesting this enhancement.

(SBCL only) Fast-alists can now be garbage collected (we believe) in SBCL, as they had already been done in CCL. (Implementation note: The change was to use weak hash tables in the implementation of SBCL fast-alists.) Thanks to Jared Davis for suggesting this enhancement.

The utility ec-call can now be applied to calls of symbols introduced with defun-inline, or with define using keyword argument :inline t, thanks to a request from Jared Davis. For example, the following is now legal.

(defun-inline foo (x)
  (cons x x))

(defun bar (x)
  (ec-call (foo x)))

The proof-builder is now sensitive to the current case-split-limitations.

New Features

The Common Lisp function sleep is now defined in ACL2. Thanks to Jared Davis for requesting this addition.

Custom error messages may now be created for guard violations. See set-guard-msg.

The new macro assert* is like assert$, except that assert* only generates a guard proof obligation, not a runtime check. Assert* is defined using a new macro mbt*, which is a variant of mbt: a call of mbt* logically returns t, but generates the same guard proof obligation as mbt. Thanks to Shilpi Goel for a query that led us to add these macros.

Heuristic and Efficiency Improvements

We fixed an inefficiency that could occur in calls of program-mode functions that update stobjs. See the discussion of invariant-risk in the documentation topic, program-wrapper. Thanks to Jared Davis for bringing this issue to our attention.

We improved the ``worse-than'' heuristic, providing modest speed-up and eliminating the use of memoization for it. Thanks to Jared Davis for useful discussions on the topic, and to Camm Maguire for an observation that led us to do some investigations that led to this improvement. For more information see comments in source function worse-than-builtin-clocked (source file type-set-b.lisp).

We avoid the cost of translating ACL2 terms (see term) to user-level syntax after applying the ``preprocess'' simplifier (see hints-and-the-waterfall), and also after applying either :use or :by hints. Thanks to David Rager for helpful discussions towards this change. Note: On rare occasions, this might change the prover flow as follows.

Consider the case that the input goal, "Goal", simplifies with the ``preprocess'' simplifier to a new goal that prints the same as "Goal". Formerly, this case avoided labeling the new goal as "Goal'"; it was as though the new goal was actually the user input. The new criterion for avoiding "Goal'" is somewhat weaker: the internal syntax must suitably match for "Goal" and its simplification, rather than their displayed forms.
Consider the application of a :use or :by hint. In such cases, the resulting constraint (if any) is simplified with the ``preprocess'' simplifier. Formerly, the rules used by that simplifier were not recorded if the printed version of the simplified constraint was equal to the original constraint, which was really a bug since the comparison was between the user-level syntax of the simplified constraint and the internal syntax of the original constraint. Now, ACL2 compares the internal syntax of each.

We fixed an inefficiency that could occur in processing of make-event forms. Thanks to Sol Swords for reporting and diagnosing the problem. (Technical note: The fix involves avoiding, in most cases, looking up world global 'boot-strap-flg by using a new state global instead of the same name.)

We changed the heuristics for equality substitution so that so-called cross-fertilization, where an equality substitution is made on only one side of the goal's conclusion, is not made when generalization is turned off, as with the hint :do-not '(generalize). Instead, the equality is used throughout the goal in that case. Thanks to David Hardin for bringing an example to our attention that led us to make this change.

Some clause-building (essentially, goal-building) operations already avoided duplication, but now consider clauses to be ``duplicates'' when the only difference is commuted arguments of equal or iff. (Note: This change was made in support of assert* and mbt*, mentioned above.)

(SBCL only) It had been the case for host Lisp SBCL that the use of defun-inline to define functions in books had failed to result in inlined code, when those functions were called after including those books. This has been fixed (and appears not to have been a problem for host Lisp CCL). Thanks to Jared Davis for bringing this issue to our attention.

Bug Fixes

A potential soundness issue could result from the application of metafunctions and clause-processors: although ACL2 checked that their outputs contain only legal terms, it did not check for the absence of calls of certain ``forbidden'' function symbols. For example, sys-call should be prohibited unless there is an active trust tag (see defttag), but a metafunction was able to introduce a call of sys-call. We have added the necessary checks, in a way that we hope has negligible impact on performance. To avoid that impact or to learn more about this issue, see set-skip-meta-termp-checks; this new utility, which requires a trust tag, avoids not only the new checks but even the above-mentioned checks for legal terms.

The edited log below illustrates a bug that we have fixed, involving the processing of include-book events in the certification world whose filename starts with the tilde (~) character.

~/temp/incl$ cat sub/bad.acl2
(include-book "~/acl2/acl2/books/arithmetic/top")
~/temp/incl$ acl2h
[[.. output elided ..]]
ACL2 !>(ld "sub/bad.acl2")
[[.. output elided ..]]
ACL2 !>(certify-book "foo" 1)


HARD ACL2 ERROR in ABSOLUTE-PATHNAME-STRING-P:  Implementation error:
Forgot to apply expand-tilde-to-user-home-dir before calling absolute-
pathname-string-p. Please contact the ACL2 implementors.



ACL2 Error in TOP-LEVEL:  Evaluation aborted.  To debug see :DOC print-
gv, see :DOC trace, and see :DOC wet.

ACL2 !>

Fixed several issues with the :puff command, and updated its documentation accordingly. See puff.

Fixed a bug in the proof-builder's wrap command. Thanks to Keshav Kini for sending a simple example that illustrated this bug.

(Allegro CL only) Fixed a bug in trace!, which for example was evidenced when evaluating (trace! (nth :native t)).

Fixed a bug in the printing of user-level terms that failed to account for untrans-table entries for nth, update-nth, and update-nth-array, when printing the first argument as a symbolic constant corresponding to a stobj argument. Thanks to Warren Hunt for reporting this issue with an example much like the following. When submitting the forms below, ACL2 output for the final form displayed the user-level term (update-nth *fld* v st) instead of the expected form, (!nth *fld* v st).

(defstobj st fld)

(defmacro !nth (x y z)
  `(update-nth ,x ,y ,z))

(add-macro-fn !nth update-nth)

(thm (equal (update-fld v st)
            xxx)
     :hints (("Goal" :in-theory (disable update-nth))))

Fixed a failure to guard-check type declarations for let and mv-let forms. Consider for example:

(defun foo (x)
  (let ((a (car x)))
    (declare (type string a))
    a))

Previously, the call (foo '(3 4)) did not cause a guard violation, even though it should have done so. (Indeed, the event (verify-guards foo) failed, and continues to fail.)

Fixed a bug in redundancy checking for mutual-recursion events that specify :ruler-extenders in an xargs declare form. Thanks to Sol Swords for sending an example that illustrates the bug: a mutual-recursion event that, when executed twice, caused an error the second time rather than being redundant (see redundant-events). The bug was actually in how ACL2 stores information about the ruler-extenders used in definitions: the :ruler-extenders specified for the first defun was being mistakenly stored for the second defun. This mishandling of redundancy for mutual-recursion events appears to be the only consequence of that bug.

The following bug was probably not observable, but violated our claim that the system behaves as logically specified. When a guard check failed during execution, the error message that was printed could differ slightly from what is logically specified. (Technical detail: the error actually printed by source function ev-fncall-rec was appropriately showing the original guard, but the specification function ev-fncall-rec-logical was showing the untranslation of the translated guard.) This has been fixed.

The save and retrieve commands for the proof-builder (see ACL2-pc::save and ACL2-pc::retrieve) now cause an error when the supplied name is not a symbol; similarly for the :event-name argument of verify. The behavior wasn't as expected for non-symbol names; for example, after issuing the instruction (save 'abc) in the proof-builder, the command (retrieve 'abc) failed to resume the proof-builder session. (Notice the erroneous use of the quoted symbol 'abc, i.e., (quote abc), rather than of the symbol abc.) Thanks to Keshav Kini for bringing this problem to our attention.

We fixed the following two bugs in the processing of backchain limits stored for rules. Thanks to Dave Greve for bringing these to our attention.

For rules of class :type-prescription, the specification of :backchain-limit-lst within the :rule-classes could be ignored or cause a hard Lisp error.
For rules of class :meta, preceding calls of set-default-backchain-limit were ignored.

Fixed a bug in the processing of certain operations on pathnames containing "..".

Changes at the System Level

By default, the ACL2 executable once again is named saved_acl2, though unlike previous versions, this executable is hons-enabled. Correspondingly, the ACL2(c) executable (that is, the executable that is not hons-enabled) is by default saved_acl2c. Thanks to David Hardin for suggesting these changes.

Links from the home page to user's manual topics now point to the ACL2+Books combined manual, not the ACL2 (only) User's Manual, except for the one link that explicitly points to the latter. Thanks to David Hardin for feedback leading to this change, which was incorporated into the ACL2 Version 7.0 home page several days after the release of that version.

Garbage collection notification has been turned off by default, not only for ACL2(c) as before, but also for (the default build) ACL2(h). Thanks to Eric Smith for suggesting this change. See ACL2-customization and see gc-verbose for how to turn such notification back on in your own environment.

It is now possible to move the system books directory after certifying its books, without invalidating their status as certified. Users should generally not notice this change. We thank Harsh Raju Chamarthi and Camm Maguire for reporting problems with hacks we have produced over the years to support distribution of books with their certificate files. Those hacks are no longer necessary: as a byproduct of this change, we have deleted both the community-books directory books/fix-cert/ and the source function make-certificate-file-relocated. For a bit more detail see the final remark in the topic full-book-name. We also thank Eric Smith, Jared Davis, and Sol Swords for reporting bugs in our initial implementations of this enhancement.

The certify-books target for make now excludes other expensive directories in addition to workshops.

(SBCL only) Modified the handling of environment variable SBCL_HOME. Thanks to Jared Davis for pointing out a problem leading to this change, namely, failure on his platform when evaluating (require :sb-sprof) in raw Lisp.

Intended compiler optimizations are now guaranteed to be in place. We observed, thanks to communication from Jared Davis, that when ACL2 is built using SBCL 1.2.10, ACL2 starts up without the compiler optimizations that had been installed during the build. Perhaps that has been true for other SBCL versions or even other Lisps. Now, ACL2 explicitly restores those optimizations when it starts up. We observed a 5% time reduction for SBCL-based regression after this change.

Environment variable ACL2_WRITE_PORT is now ignored when doing provisional-certification. Thanks to Sol Swords for discussing this issue, which arose from a failure in community-books directory books/workshops/2011/verbeek-schmaltz/sources/, which uses provisional-certification.

(GCL only) A few tweaks were made in support of GCL changes starting with pre-releases of GCL 2.6.13 in late April 2015 (but these tweaks are backward compatible with older GCL releases). Resulting ACL2 builds for a new GCL show dramatic speed-ups for a single user, perhaps cutting between a third and half the time, with less dramatic improvements when running regressions with -j 8. Thanks to Camm Maguire for pointing us to the changes and for improving GCL.

EMACS Support

The commands Control-t e and Control-t Control-e, defined in file emacs/emacs-acl2.el, now check that the *acl2-shell* buffer exists, has a live process, and has a last line matching the specification in *acl2-insert-pats*, which has Emacs documentation (using Control-h v) but is set to a default based on shell prompts. Thanks to David Rager, Jared Davis, and Shilpi Goel for helpful discussions leading to this change.

We installed the following two patches to file emacs/emacs-acl2.el, both contributed by Keshav Kini.

Emacs highlighting for forms starting with "(def" now works when the "def" symbol has a package prefix, for example, "(fty::deflist".
The Control-d character is no longer explicitly bound to the default, delete-char, but instead is unbound in comint-mode-map, so that the global binding of Control-d will take effect. Thus, users who bind Control-d themselves will no longer have that binding overridden in shell-mode (or comint-mode).

We made several improvements to the ACL2-doc Emacs browser for ACL2 documentation.

Fixed a bug that could occur when Emacs variable large-file-warning-threshold is nil. Thanks to Bob Boyer for bringing this bug to our attention.
Links are now in color (blue, by default). See ACL2-doc for instructions on how to change or remove this color. Thanks to Jared Davis for suggesting the use of color. We are open to suggestions for improvements; this might be just a first step.
Allow limiting search and index commands to ancestors (sub-topics, sub-sub-topics, etc.) of a command (including the command itself), by supplying a prefix argument.
New "p", "<", and Control-TAB commands are analogues of "n", ",", and TAB — for search, index, and next-link commands, respectively — to go backward instead of forward.

Experimental Versions

(For ACL2(p) users only; see parallelism) If parallel execution is enabled (see set-parallel-execution), as it is by default in ACL2(p), then hons-wash and hons-clear may be no-ops (other than to print a warning), in order to avoid thread-unsafe behavior. (However, In CCL you are unlikely to see this restriction unless you are running more than one thread.) To get around this restriction, you can instead use hons-wash! or hons-clear!, which however require a trust-tag. Thanks to Bob Boyer for bringing this issue to our attention.

Subtopics

Note-7-1-books: Release notes for the ACL2 Community Books for ACL2 7.1 (May 2015)