		Search-engine friendly clone of the ACL2 documentation.

Release-notes

Note-7-3

ACL2 Version 7.3 (December, 2016) 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.2 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. Changes to the books are no longer summarized in a documentation topic, but can be found by browsing the ACL2+Books GitHub repository, in particular, the raw commit log.

Changes to Existing Features

The name of ACL2's interactive goal manager has been changed from ``proof-checker'' to ``(interactive) proof-builder''. Thanks to several people in the ACL2 community for feedback leading to this more descriptive name. In particular, we thank Stephen Westfold for noting that as a new user, references in the documentation to ``proof-checker'' didn't help him to realize that ACL2 has an interactive proof capability similar to what is found in some other interactive theorem provers.

Now, set-raw-warning-format causes all warnings to be printed in a raw format, not merely those warnings for which custom raw-warning-format code has been developed. Thanks to Shilpi Goel for recommending this enhancement.

Utilities for formatted printing to strings no longer take an :iprint keyword argument, and they never print using iprinting. See printing-to-strings. The reason is that for each iprint index, i, that is bound during creation of the result string, that binding would disappear after the string is returned; so it would be misleading or an error to read #@i# after that return. For a similar reason, when raw Lisp errors occur because variable *hard-error-is-error* is non-nil (see hard-error), iprinting is not used.

Any :measure supplied in an xargs declaration of a defun form must be a legal term. Formerly, this requirement only applied to :logic mode definitions, but now it also applies to :program mode definitions. Thanks to Jared Davis for pointing out that this restriction wasn't applied to :program mode definitions.

For a defun form, it is now illegal by default for a non-recursive definition to have a :measure in an xargs declaration (other than :measure nil, which means ``no measure'') unless the definition is within a mutual-recursion. Thanks to Eric Smith for suggesting this restriction. See set-bogus-measure-ok for a way to avoid this new default behavior.

Several symbols have been added to the list *ACL2-exports*.

It is now legal to specify a :clause-processor hint using a symbol, regardless of the signature of the relevant clause-processor function. A symbol had only been legal when that function took a single input. Now, the function may also take a hint argument followed by zero or more stobj arguments, in which case the hint is implicitly nil and the stobjs are passed appropriately. See clause-processor. Thanks to Eric Smith for requesting this enhancement.

By default, the checksum values in certificate files for books have been replaced by a faster (though somewhat less secure) mechanism. See book-hash for an explanation, including a way to restore the use of checksums. (Our experiments in certifying all community books showed about a 7% reduction in total time. Speed-up for include-book may be somewhat greater; for example, on a modern Macbook Pro the form

(time$ (include-book "centaur/vl/mlib/datatype-tools" :dir :system))

took 21.67 seconds after certifying books in a default manner, but only 15.80 seconds after certifying books using ACL2_BOOK_HASH_ALISTP=t — a 27% reduction.) Thanks to Bob Boyer for emphasizing slowdown from checksum computation, to Jared Davis and Eric Smith for several helpful emails, and to the ACL2 community in general for continuing to push for faster evaluation of include-book calls.

The utility show-accumulated-persistence now prints results in base 10 with radix nil (see set-print-base and set-print-radix). Thanks to Sol Swords for pointing out the odd printing that formerly could result when evaluating (set-print-base-radix 16 state) before calling show-accumulated-persistence.

We have changed how ACL2 automatically computes type-prescription rules for defun forms — so-called ``runic type-prescriptions'' — in the following cases:

(1) when including a certified book; and
(2) in the second pass for a call of encapsulate or certify-book.

For (1), ACL2 retrieves runic type-prescriptions from the book's certificate. For (2), ACL2 combines the runic type-prescription rule that is computed as usual with the rule previously computed in the first pass. Because of (1), the runic type-prescription rule for a function symbol introduced by an included book is no longer sensitive to the current logical world; previously, for example, that rule could be different if one first includes other books. Also, some include-book calls may complete more quickly because of (1); for example, we saw a reduction in time of 4.7% for (include-book "doc/top" :dir :system). Because of (2), runic type-prescriptions may be stronger than was previously the case. Thanks to Jared Davis for suggesting this enhancement and for helpful discussions during its development. This change can be viewed as just one of the hundreds of heuristic components of ACL2 that need not be understood in any detail by users; that said, those who are curious about implementation details are welcome to read the comment entitled ``Essay on Cert-data'' in the ACL2 source code.

The utility save-exec now causes an error if the directory of its first argument does not exist; for example, (save-exec "subdir/my-acl2") causes an error if there is no subdirectory "subdir" of the current directory. Thanks to Jared Davis for pointing out that some Lisps (in particular, CCL) would create a missing directory in such a case, while others (in particular, SBCL) would not.

Slightly improved the printing of terms (the so-called ``untranslate'' utility) to avoid producing terms of the form (not (not u)) in some cases. Thanks to Eric Smith for feedback leading to this change.

The function being defined (or functions, plural, if using mutual-recursion) may now be among the declared ruler-extenders. Thanks to Alessandro Coglio for an email that led us to make this change.

The utility :pso, along with other proof-replay utilities including psof and psog, now works with defthmd and defund. More generally, saved proofs are only wiped out by newer proofs, not by other events such as in-theory events.

The :exec code in calls of mbe no longer affects termination proofs or induction schemes produced for function definitions. This had formerly only been the case for certain ``top-level'' calls in the if-then-else structure of the definition's body.

The macro logicalp is now deprecated, replaced by the function symbol logicp. (For efficiency, logicp is inlined in raw Lisp; logicalp is for now simply a macro abbreviating logicp.) Moreover, these utilities no longer call the function symbol-class. (See system-utilities for discussion of such utilities.) The latter change, which avoids consideration of the 'theorem property of a symbol, can be helpful in proofs; indeed, this change simplifies reasoning about the new function logic-fnsp (see the ``Bug Fixes'' section below).

Several improvements have been made for utilities that show guard proof obligations.

The low-level system utility guard-obligation no longer returns state. Thanks to Alessandro Coglio for requesting this enhancement.
The utilities verify-guards-formula and guard-obligation take a new argument, rrp (``return redundant p''). When this argument is nil, which is the default for verify-guards-formula, these utilities will avoid returning the symbol 'redundant even in the case that the given function symbol is already guard-verified. Thanks to Eric Smith for requesting this enhancement.
Documentation has been improved for utilities that show guard proof obligations, in particular with the addition of a new topic, guard-formula-utilities, which explains their differences.
The utilities guard-theorem and gthm now do some simplification of the guard theorem by default. See guard-theorem and gthm. Thanks to Alessandro Coglio and Eric Smith for useful discussions.
The utility gthm has two improvements: it takes a second optional argument, guard-debug; and it returns a single value (an untranslated term), rather than an error-triple whose value component is that untranslated term. The function guard-theorem has been changed to support the new optional argument.

Some recursive, logic-mode built-in functions did not have proper measures stored in the ACL2 logical world: specifically, those whose suitability for logic mode is established in the community book books/system/top.lisp and the books included under that book. This has been fixed for all such functions except for the two (merge-sort-term-order and merge-term-order) whose measures use functions defined only in books, not in ACL2. Thanks to Eric Smith for a request leading to this enhancement. (If you are interested in implementation-level information about the mechanism tying books to verification of termination and guards for built-in functions, see comments in source-code constant *system-verify-guards-alist*.)

The utilities print-gv and set-print-gv-defaults now accept a natural number for the keyword argument, :substitute, so that only certain large repeated terms cause the result to use flet. See print-gv. Thanks to Eric Smith for suggesting such a change and helping to design it.

ACL2 formerly caused a raw Lisp error when attempting to define a function that was already defined in raw Lisp but not in ACL2. Now an ordinary ACL2 error occurs instead. Thanks to Eric Smith for a question leading to this change.

Functions all-ffn-symbs and all-ffn-symbs-lst are now in guard-verified :logic mode. Thanks to Eric Smith for a helpful relevant conversation. Several other functions are now in guard-verified :logic mode, thanks to discussions with Eric and also Alessandro Coglio, including formalized-varlistp, latest-body, logical-namep, macro-args, stobjs-out, termify-clause-set, throw-nonexec-error-p, and throw-nonexec-error-p1. For a complete list, compare the old and new values of constant *system-verify-guards-alist*.

It had been necessary to evaluate (set-state-ok t) in order to call verify-termination on a :program mode function that takes state as a formal parameter but does not declare state explicitly as a stobj. Thanks to Eric Smith for pointing out this issue. Here is an example that had failed but now succeeds.

(set-state-ok t)
(defun foo (state) (declare (xargs :mode :program)) state)
(set-state-ok nil)
(verify-termination foo) ; formerly failed

To evaluate a form (set-iprint t :hard-bound N), ACL2 will first replace t by :reset-enable. This behavior has been expanded to apply to (set-iprint nil :hard-bound N) and (set-iprint :same :hard-bound N) as well: the first argument will be converted to :reset or :reset-enable. See set-iprint. This change fixes a bug in the interaction between hard-bounds and rollovers. For an example that formerly exhibited this bug, see a comment about ``hard-bounds and rollovers'' in (defxdoc note-7-3 ...) in community book books/system/doc/acl2-doc.lisp.

The following improvements have been made to defun-sk. See defun-sk for detailed documentation.

Defun-sk now modifies the pe-table, with the effect that if you introduce a function NAME with defun-sk, then subsequent evaluation of :pe NAME will show the defun-sk form rather than the underlying defun form. As usual, you can invoke :pe! instead, in order to see that defun form.
When defun-sk was supplied with keyword argument :strengthen t, the name of the generated theorem was always in the "ACL2" package. Now it is in the same package as the function symbol being defined. Thanks to Alessandro Coglio for suggesting this change.
Defun-sk now accepts declare forms immediately after the formal parameters, as is the case for defun. Thanks to Eric Smith for suggesting this enhancement. The :witness-dcls keyword is still supported as well, but may become deprecated in the future.
An issue involving guard verification for defun-sk forms has been addressed. Thanks to Alessandro Coglio for suggesting this improvement.
Syntax checking now produces improved error messages for defun-sk.

The error message for a call of a undefined symbol now mentions defined symbols in other packages with the same name, in case that is what the user intended. The message also points to a new documentation topic, near-misses, which provides a way (using certain books) to find approximate matches that are defined. Thanks to Jared Davis for suggesting such a change.

ACL2 now accepts #\Return as legal notation for the character with char-code 13, and it prints that character as #\Return rather than moving the cursor (e.g., to the beginning of the line). Thanks to Alessandro Coglio, Eric McCarthy, and Eric Smith for requesting this change, to help with the printing of failed subgoals that mention this character.

The macro good-bye no longer requires its argument to be a (natural) number. Any argument is now valid, and as before, is evaluated; if that argument is not an integer, it is treated as 0. The same change applies to the aliases for good-bye, namely exit and quit. Thanks to Eric Smith for suggesting this change.

When some subgoal in a set of key checkpoints is NIL, then such a subgoal will be printed first in the corresponding list, provided of course that the list isn't entirely ignored because of a checkpoint-summary-limit of 0. See nil-goal, which has been updated. Thanks to Eric Smith for suggesting that NIL subgoals should be seen in the checkpoints in spite of the checkpoint-summary-limit.

A new keyword argument, :ctx, is available for value-triple. See value-triple.

Definition rules with non-nil values of :install-body (the default) are now permitted to have equivalence relations other than equal.

For macros such as prog2$ that invoke return-last, an argument to be evaluated with attachments (see defattach) was failing to use attachments in some cases involving non-guard-verified functions. This has been fixed. For an example, see the relevant comment in the form (defxdoc note-7-3 ...) in community book books/system/doc/acl2-doc.lisp.

The :termination-theorem lemma-instance has been improved so that old function symbols may be replaced with corresponding new function symbols, either automatically or explicitly by the user. See lemma-instance and see termination-theorem-example. Thanks for Alessandro Coglio and Eric Smith for helpful discussions, including pointing out the previous deficiency.

A new key, :user, is now legal for the ACL2-defaults-table. Its value must be an association list. The key is reserved for users, who may assume that the ACL2 system does not give it any special handling; see ACL2-defaults-table. Thanks to Eric Smith for a helpful discussion leading to this change.

A new macro, (with-guard-checking-event x form), is now legal for event contexts; see embedded-event-form. Thanks to Eric Smith for helpful discussions leading to this change.

For many years, it has been the case that when a constraint is proved that arises from a :functional-instance lemma instance (see [lemma-instance]), that information is stored so that the same constraint is not re-proved on behalf of a later such lemma instance. However, this had not been the case when the original lemma instance was inside an encapsulate event. Now, that information is stored provided the encapsulate event has an empty signature list and is not ``empty'' (that is, stores at least one event). Thanks to Eric Smith for sending us an example to point out this problem.

The proof-builder's bash and reduce commands no longer fail when the :hints for "Goal" include :do-not-induct t. Thus, it is no longer necessary to edit out such :do-not-induct hints when editing a proof-builder command by copying hints from an event being developed.

By default, the proof-builder command :s now uses contextual information when doing linear arithmetic. The new keyword argument :linear can be set to nil to get the previous behavior. See ACL2-pc::s. Thanks to Eric Smith for requests that led us to make this change.

Warning and error messages produced upon theory-invariant violations now include additional explanation. Thanks to David Hardin and Grant Passmore for helpful remarks leading us to make this change. Those messages also now show where the theory invariant was defined: a book pathname, or ``top-level'' if directly in the loop.

The summary of ``Key checkpoint'' goals, at the end of a failed proof attempt, has been improved. It now indicates, inside the ``***'' banners, every case in which proof has been aborted due to a :DO-NOT-INDUCT hint or generation of a goal of NIL.

The proof-builder command, noise, no longer prints proof-tree information, which can be obtained with the new command, noise!. The quiet command is unchanged, but a quiet! command turns off the printing of goal identifiers (as with set-print-clause-ids).

When defund and defthmd events fail, their output no longer concludes with distracting output that mentions with-output.

New Features

New optional arguments allow the pso utility to restrict output to a single goal or a segment of the output (say, between two specified goals); similarly for related utilities pso!, psof, and psog. Thanks to David Rager for a recent query leading to this enhancement.

The function cons-with-hint provides an alternative to cons that can sometimes avoid consing. Thanks to Jared Davis and Sol Swords for suggesting this function and providing an implementation and documentation. A few ACL2 source functions now call cons-with-hint.

Function file-length$ computes efficiently the number of bytes in a specified file.

Function delete-file$ deletes a given file. Thanks to Eric Smith for requesting this utility.

New macros active-or-non-runep and incompatible! are similar to active-runep and incompatible (respectively), except that the new macros essentially consider non-runes to be enabled. Thanks to Eric Smith for feedback leading to these additions.

It is now possible to declare formal parameters of defun events to be irrelevant. See irrelevant-formals. Thanks to Eric Smith for requesting this feature.

The deftheory event now accepts a new keyword, :redundant-okp, to allow a limited form of redundancy (see redundant-events). Thanks to Eric Smith for requesting such support. A new macro, defthy, abbreviates deftheory calls by adding :redundant-okp t.

The fmt family of functions has a new tilde directive, ~S, which behaves like ~s except that margins are ignored. Thanks to Jared Davis for requesting this feature.

The iprinting utility has a new keyword option, :share, which causes iprint indices to be re-used (using so-called ``iprint sharing'' and ``iprint eager sharing''). See set-iprint. Thanks to David Rager for suggesting a notion of iprint sharing.

A new function, set-serialize-character-system, can be used to turn off (or on) the serialize-write capability, which is on by default, for writing certain files during book certification, including certificate files. This capability has been useful for working around issues with 32-bit CCL; thanks to Waqar Ahmed for working through that issue with us.

ACL2 now supports the reading of rational numbers expressed in floating-point (scientific notation) syntax, using prefixes "#f" and "#fx" for base 10 and base 16, respectively. See sharp-f-reader. Thanks to Dmitry Nadezhin for suggesting this enhancement.

Heuristic and Efficiency Improvements

The raw-Lisp definition of defpkg has been modified in a way that may improve performance for some host Lisps. Thanks to Bob Boyer for emails pointing to the (surprising) use of compilation by include-book in CCL, which is eliminated (at least in some cases) by this change.

Type-set reasoning has been improved in several basic ways.

The first, for which we thank Jared Davis and Sol Swords for providing an example, is illustrated in a comment in the form (defxdoc note-7-3 ...) in Community Books file system/doc/acl2-doc.lisp)
When definition bodies and guards are simplified, as they are by default — see the new documentation for normalize — type-set reasoning is now subjected to a backchain-limit of 1 (unless it is already 0 globally). Thanks to Jared Davis for sending an example, for which include-book time has been cut to less than 10% of what it had been, without changing the results of normalization. (That said, regression timings suggest that this change will not be noticed for most books.)
The collection of primitive type-sets supported by ACL2 has been changed, by splitting the type of positive integers into two sets: the set consisting solely of the number 1, and the set of integers greater than 1. Thanks to Jared Davis for suggesting this change, and to him and Sol Swords for pointing out deficiencies in our initial implementation. For a discussion of changes made to community books to accommodate this change, see the comment immediately above the form (defxdoc note-7-3 ...) in community book books/system/doc/acl2-doc.lisp. Note that ACL2 has a newly-added function, bitp, whose built-in compound-recognizer rule specifies that the value recognized by bitp is either 0 or 1, that is, a member of the union of the primitive types {0} and {1}.
Theorem: bitp-compound-recognizer
```
(defthm bitp-compound-recognizer
  (equal (bitp x)
         (or (equal x 0) (equal x 1)))
  :rule-classes :compound-recognizer)
```
ACL2 can reason a bit more powerfully about existing functions in some cases. For example, it now proves the following theorem without including any books, which was not the case previously.
```
(thm (implies (and (rationalp x) (not (integerp x)))
              (< 1 (denominator x))))
```
You may need to change some of your books, however. For example, if you want to disable a function that always returns 1, then as was previously the case for such functions that always return 0 instead (or t, or nil), you'll want to disable the type-prescription rule for that function, too.
When a term of the form (integerp (+ k term)) is assumed true or false, for an integer constant k, ACL2 now essentially attempts to add suitable type information for term rather than for (+ k term). (Source function strengthen-recog-call shows precisely what is done.) We also made analogous improvements for terms of the form (rationalp (+ k term)) and (rationalp (* k term)). Example theorem now provable that was not provable previously:
```
(thm (implies (and (zp k) ; either k <= 0 or k is not an integer
                   (integerp (+ 1 k))
                   (< 0 (+ 1 k))
                   (acl2-numberp k))
              (equal 2 (+ 2 (* 2 k)))))
```

We eliminated a rather technical check during book certification. (A bit of technical detail: we check for hidden packages in make-event expansions, and an optimization eliminated that check for events in the book occurring before the first such event that introduced a new package, if any. But if no events in the book introduced a new package, then we were checking all such expansions; now, we check none of them.)

Calls of the utility clear-memoize-table formerly discarded relevant hash tables, building new ones when necessary. Now, the hash tables are typically retained but cleared (using Common Lisp function clrhash), although heuristics may determine that tables are ``too large'', in which case the former discarding behavior applies. Thanks to Jared Davis and Sol Swords for contributing this change, which they found to speed up certain computations significantly. We expect that it will likely not slow others down significantly. Note that (as they have pointed out) the behavior of related utility clear-memoize-tables remains unchanged; it continues to discard relevant hash tables.

The generation of raw Lisp definitions of stobj creator functions have been made potentially more efficient for stobjs with many fields. Thanks to Sol Swords and Jared Davis for reporting this issue and suggesting a fix, which we adopted (in source function defstobj-raw-init) with some small changes.

We now avoid certain inefficiencies with mbe. The definition of f8 below has taken 83.63 seconds in Version 7.2 built on CCL as the host Lisp, but with that same machine and host Lisp the time was merely 0.11 second after this change. (Technical note: the explosion was in the time required to compile the so-called ``*1* function''.)

(defmacro id (x) `(mbe :logic (identity ,x) :exec (identity ,x)))
(defun f8 (x) (id (id (id (id (id (id (id (id x)))))))))

The heuristics for the ``eliminate-irrelevance'' clause processor (see hints) no longer drop applications of zero-ary functions or their negations, e.g., (P) or (NOT P). Thanks to Marijn Heule for feedback that led us towards modifying our initial change (twice!).

Several low-level efficiency improvements, which can speed up read-object, may also speed up some other operations.

Finding a package from a string can be faster (low-level raw Lisp function find-package-fast).
The implementation of low-level raw Lisp function bad-lisp-objectp was tweaked to use type recognizers, which are faster in some Lisps than corresponding recognizer predicates; for example, the test (consp x) has been replaced by the test (typep x 'cons).
New raw Lisp function bad-lisp-consp processes conses on behalf of bad-lisp-objectp, and now bad-lisp-consp is memoized at startup instead of bad-lisp-objectp. Note that we continue to use memoization option :forget t, which throws away memoization information when exiting the top-level call of the function. With this change, we avoid the overhead of memoization when checking non-cons values, which was perhaps of limited value anyhow. There could be slowdown when large EQ strings occur repeatedly inside a cons pair, but we expect such slowdown to be at most negligible in practice.
New utility set-bad-lisp-consp-memoize can turn off memoization of the new raw Lisp function bad-lisp-consp.

Bug Fixes

A soundness bug exploited the possibility that pathnames contain illegal ACL2 characters. Consider the following bash shell commands, which create a file whose name is the euro sign and create a soft link, "foo", to that file. Thanks to Eric McCarthy for helpful discussions showing us how to create such a file, which ultimately led us to discover this bug.

mkdir $'\xe2\x82\xac'
ln -s $'\xe2\x82\xac' foo

Then the following book certified on a Mac, but now one gets an error message complaining about a character with code 8364.

(in-package "ACL2")
(make-event
 `(defconst *c* ,(char (canonical-pathname "foo" t state) 44)))
(defthm bad
  nil
  :rule-classes nil
  :hints (("Goal"
           :in-theory (theory 'minimal-theory)
           :use ((:instance char-code-linear (x *c*))))))

The utility getenv$ now causes an error if the value it would otherwise return is not an ACL2 string, for example because it contains a character whose char-code exceeds 255. Many other changes, less visible to the user, have been made in how ACL2 deals with strings that come from outside ACL2, in particular, file names (see the related item just above).

The handling of metafunctions allowed an invariant to be violated, that conjectures in the prover are always 100% logic mode. An example is in a comment in the ACL2 source code under (deflabel note-7-3 ...). We have not exploited this bug to show that it leads to unsoundness, but that seems possible. Our fix is to extend the checks that all applications of metafunctions and clause-processors produce terms, to check additionally that those terms are all in logic mode. An analogous change applies to well-formedness-guarantees, using new functions logic-termp, logic-term-listp, and logic-term-list-listp, where logic-termp checks not only termp but also the new predicate logic-fnsp, and similarly for the others (logic-term-listp calls logic-fns-listp and logic-term-list-listp calls logic-fns-list-listp).

A bug has been fixed that could cause hard Lisp error when using the iprint utility. Specifically, calling set-iprint with a small :hard-bound could cause a hard Lisp error during ``rollover'', as with the following example.

(set-iprint :reset-enable :hard-bound 200)
(set-iprint t :hard-bound 1000)
(f-get-global 'iprint-ar state)
(set-evisc-tuple (evisc-tuple 3 4 nil nil) :iprint t :sites :all)
(thm (equal (append (append x y) x y x y x y x y)
            (append x y x y x y x y x y)))
(pso)
(pso)
(pso)

Thanks to David Rager for bringing this bug to our attention and for describing how it occurred in his environment. The fix is to convert the argument t of set-iprint to :reset-enable when keyword argument :hard-bound is supplied.

The keyword :computed-hints-replacement appeared in the source code a few times where :computed-hint-replacement was intended. This has been fixed. We are not aware of any examples in practice where this makes a noticeable difference; in particular, no community-books were modified to accommodate this fix.

Redefinition can support certain uses of make-event within encapsulate forms, where formerly an error occurred. (Technical note: Small examples appear as comments in source function chk-embedded-event-form; search there for ``redefinition''.) Thanks to Jared Davis for sending us an example that exhibited this problem. Strictly speaking, we don't really view this as a bug; we have clarified in the documentation for ld-redefinition-action that redefinition may behave in unexpected ways.

We now avoid creating directories when reading rather than writing:

It is no longer the case that include-book creates a directory when attempting to include a book in a non-existent directory. Thanks to Jared Davis for bringing this bug to our attention.
In Version 7.2, we arranged that open-output-channel and open-output-channel! attempt to create directories as needed. Unfortunately, that change also caused this behavior for open-input-channel. That has been fixed. Thanks to Sol Swords for pointing out that certifying books in CCL using cert.pl could cause creation of directories when including books; with this fix, that is no longer the case.

When submitting a call of define-trusted-clause-processor with an unsuitable signature, the resulting error message was causing a raw Lisp error. This has been fixed. Thanks to Eric Smith for reporting this bug.

Contrary to its documentation, a define-trusted-clause-processor event was never redundant in the case that the values for keyword arguments :label and :partial-theory were both nil (or omitted). Thanks to Eric Smith for pointing out this bug. Now, redundancy of the resulting encapsulate event succeeds because a subsidiary deflabel event is generated by default. (The previous behavior can be obtained by explicitly supplying the keyword argument :label nil.) Also, the obsolete keyword argument, :doc, has been deleted for define-trusted-clause-processor.

It had been possible to get a slow-array-warning from computed hints (see computed-hints) that directly modify so-called enabled structures. This has been fixed by providing a suitable way for users to call system function load-hint-settings-into-rcnst, as is done in the community-books utility easy-simplify-term, which calls a function easy-simplify-term1-fn that updates an enabled structure. Thanks to Jared Davis for sending an example that exhibited this problem through the computed hint logbitp-reasoning. Also thanks to Sol Swords for a helpful discussion that brought our attention to the community book mentioned above.

Avoided an assertion (ASSERT$ ACTUAL-ELEMENT ...) that could occur when including uncertified books, in particular when an included sub-book was originally certified in a different directory from where it now resides. Thanks to Eric Smith for reporting this bug and sending a helpful example.

Fixed function get-skipped-proofs-p so that it returns nil on built-in functions. Thanks to Eric Smith for bringing up this issue, for example by pointing out that (get-skipped-proofs-p 'len (w state)) evaluated to t; now, it evaluates to nil.

The utility unmonitor was failing to carry out its task when applied to a rune. This was due to a bug in ACL2 source function delete-assoc-equal-lst, which has been fixed.

The utility :psof now prints the Rules, Hint-events, and Splitter rules fields to the specified file instead of the terminal. It also prints the interactive proof-builder prompt to that file instead of the terminal.

On rare occasions it seems that after book certification, the compiled file was older than the corresponding .cert file, which prevented subsequent include-book forms from loading that compiled file. (Technical note: The problem was that we erroneously relied on Lisp function rename-file to preserve write-dates.) This has been fixed. Thanks to Gary Byers for confirming that Lisp does not guarantee that rename-file preserves write-dates, and to Camm Maguire for reporting a related failure.

We fixed the :puff command so that it will no longer fail on include-book commands followed by later include-book events. Thanks to Eric Smith for reporting the problem via a helpful example.

Some symbols were printed in a way that could not be read back in, but are now printed with surrounding |...|. Thanks to Sol Swords for reporting this problem for symbols with the Tab character. Now that we are more careful to print symbols readably in every host Lisp, but in a consistent manner for all host Lisps, you may find more symbols printed with surrounding |...| than is necessary for your host Lisp.

It was possible to corrupt the system by evaluating ill-guarded arguments on program-mode functions with raw Lisp code when guard-checking is off. For example, after evaluating the forms (set-guard-checking nil) and (verbose-pstack 23), the form (thm (equal x x)) caused a raw Lisp error. Now, the ill-guarded call above of verbose-pstack causes a guard violation, even with guard-checking off.

In host Lisps that do not compile on-the fly — that is, in host Lisps other than CCL and SBCL — an error occurred when trying to evaluate certain calls of comp, including (comp t) during make-event expansion. This has been fixed; here is an example that can be evaluated successfully now but not formerly.

(make-event (er-progn (comp t)
                      (value '(value-triple nil))))

ACL2 now avoids some needless escaping of symbol names with vertical bars, as in the case of car in base 16, among others supplied by Eric Smith, whom we thank for the bug report:

ACL2 !>(set-print-base-radix 16 state)
<state>
ACL2 !>'car
|CAR|
ACL2 !>

Vertical bars are used for symbols whose names are so-called ``potential numbers'', which Common Lisp defines using several criteria. Consecutive letters disqualify a token from being a potential number, and ACL2's mistake was in failing to treat characters #\A through #\F as letters.

We fixed a bug in the interaction between iprinting and brr. For an example, see the comment about ``interaction between iprinting and brr'' in the form (defxdoc note-7-3 ...) in community book books/system/doc/acl2-doc.lisp. Thanks to Shilpi Goel for pointing out a somewhat related problem introduced by a change originally made after Version_7.2, which also has been fixed.

The documentation for ld specified that ``If standard-co and proofs-co are equal strings, only one channel to that file is opened and is used for both.'' This was only the case when proofs-co was a canonical absolute (full) pathname. This has been fixed; now, the criterion is that standard-co and proofs-co are strings that represent the same file.

It is no longer illegal for defstub to use an old style output signature with variables that are not among the formals. For example, the following is now legal (note that u is not among the list (x y) of formal parameters): (defstub foo (x y) (mv u x)). Thanks to Eric Smith for pointing out that this behavior is allowed by the documentation (specifically, see the discussion of ``Old Style'' in the documentation for signature).

We fixed a bug in the implementation of defattach, which could cause the wrong constraints to be generated in the case of more than one function argument.

For a proposed definition rule with a missing (or empty) :CLIQUE but a non-empty :CONTROLLER-ALIST, the error message was ill-formed. This has been fixed.

Calls of the macro add-custom-keyword-hint are no longer illegal events in the context of local.

Tweaked break-on-error to avoid rare error involving STATE.

Changes at the System Level

It was possible for a backtrace to be printed to the terminal by SBCL and CMUCL, even when output is redirected to a file. This has been fixed. Moreover, we now print, just above a backtrace (with ACL2 function print-call-history), the full pathname of the book under certification, in case this problem arises again. Also, limited the number of frames in CMUCL to the default in SBCL, namely, 1000.

When building the executable with `make', ACL2 now prints a message of the form ``Successfully built <ACL2_executable_pathname>'' as the last line of the log. Thanks to Eric Smith for suggesting this change. Note that the exit status continues to be 0 upon success and non-zero upon failure.

An error now occurs when attempting to build ACL2 or certify the community-books (in the usual way, using make) in a directory whose name contains at least one space. Thanks to Eric Smith for discussion leading to this change. Although the issue may only be with the infrastructure for certifying community books, we cause an error for the ACL2 build as well, to make installers aware of the problem with spaces as soon as possible; thus, we added this check in both the top-level GNUmakefile and in books/GNUmakefile. Note that the installation instructions (file installation/installation.html) already said to install ACL2 ``in a directory whose pathname does not contain whitespace''; now, this requirement is enforced. (If some in the community would like to update the infrastructure for certifying books to support spaces in the build directory, they are welcome to do so and then remove the check for spaces in books/GNUmakefile, at which time we would be happy to remove corresponding code in the top-level GNUmakefile as well.)

The rdtsc feature is now used in function memoization not only for host Lisp CCL but also for SBCL. Thanks to Bob Boyer for suggesting this change and providing helpful code.

With a trust tag, it is now possible to apply verify-termination to functions with under-the-hood raw Lisp code. See verify-termination-on-raw-program-okp.

An argument has been added to the built-in function, recursivep. The old call (recursivep fn wrld) has been replaced by the equivalent new call (recursivep fn t wrld) in some community books. See system-utilities for a discussion of recursivep. Thanks to Alessandro Coglio for suggesting this change.

There is now some documentation on ACL2 system development [formerly in the topic, system-development, and its subtopics; now expanded into the Developer's Guide]. These replace the pages under web directory http://www.cs.utexas.edu/users/moore/acl2/open-architecture/. Thanks to Eric Smith for encouraging us to move that documentation to XDOC.

The Common Lisp variable *debug-io* is now used in printing backtraces, but also is bound to *standard-output* when entering the ACL2 read-eval-print loop, which is done at start-up (see lp). These changes avoid unfortunate printing of backtraces when certifying certain books that mess with *debug-io* using trust tags, such as community book. books/centaur/vl2014/server/server.lisp. Thanks to Jared Davis for a tip that helped us to debug that issue (ACL2 GitHub Issue #634).

We improved ACL2's implementation of the #. read macro so that it no longer prints additional errors after the first. Also, the error message now mentions :DOC sharp-dot-reader, pointing in particular to a relevant remark when the failure occurs during book certification.

(SBCL only) Increased the value of --dynamic-space-size written to the executable scripts to 24000, from 16000, in support of building the manual.

EMACS Support

The text-based display of documentation has been improved, that is, for output from :doc at the terminal and also for the ACL2-doc Emacs browser.

Links are inserted much more reliably. That is, the surrounding of text by square brackets for text-based display now virtually always creates links that can be followed to topics in the ACL2-doc browser. In particular, that browser now handles names properly that contain the : character.
Text in square brackets, for example [1], is no longer recognized as a link (though Emacs still highlights it). Thanks to Mihir Mehta for pointing out this issue.
Automatic insertion of links for expressions @('(name ...)'), as @('([name] ...)'), should not happen for text-based display. This was however done when generating short strings for subtopics in ACL2-doc; that no longer happens.
The see? directive (see xdoc::preprocessor) now inserts links; it did not do so before (for text-based display).
Certain ``raw'' topics, such as DEFXDOC-RAW, are now included that formerly were only included in the web-based manual.
Text within ``<stv> ... </stv>'' is now replaced by the text ``{STV display}''. A general mechanism is in place for extending this behavior to other tags (see xdoc-tag-elide-alist [after Version 8.5, xdoc-tag-alist]) in community-books file 'books/xdoc/display.lisp').
In the ACL2-doc browser, when the ``i'' (acl2-doc-index) command is invoked without a prefix argument, the mode line shows the number of matches. (The remaining matches continue to be accessible using the ``,'' (acl2-doc-index-next) command.)

Incorporated changes to emacs/emacs-acl2.el put forward by Keshav Kini (thanks!), as follows.

Now, meta-x new-shell avoids buffer names that already exist.
An error occurs when attempting to switch to a non-existent ACL2 shell buffer, rather than creating such a buffer with no process.
For a new shell, call shell instead of make-comint.
Did a bit of refactoring and improved some error messages.

Experimental Versions

As before, brr does not work in ACL2(p) with waterfall-parallelism enabled; see unsupported-waterfall-parallelism-features. But now it is an error to try to enable both brr and waterfall-parallelism. Thanks to David Rager for helpful discussions pertaining to this change.