NOTE-6-2

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

CHANGES TO EXISTING FEATURES

The macro top-level has been changed, so that evaluation of a form (top-level x) results in an error when evaluation of x results in an error. Thanks to Jared Davis for observing that when evaluating a file using ld, an interrupt of a call of a top-level call in that file would not prevent evaluation of later forms in the file.

The macro THE no longer causes an error when guard-checking is :NONE. For example, it had been the case that evaluation of (the integer t) always caused an error; but now, there is no error after executing command :set-guard-checking :NONE. Thanks to Jared Davis for asking for a way to avoid such errors.

The error printed when attempting to ``reincarnate'' a package -- that is, to define a package that is not part of the ACL2 logical world but exists in raw Lisp because it was once part of the world -- is now much more instructive. In particular, it shows pathnames for the previous and proposed defpkg events, and it shows the symbols that are imported by one but not the other. Thanks to Jared Davis for requesting this improvement.

Functions open-input-channel and open-output-channel no longer cause an error when failing to open a channel because of a permissions problem, but instead return (mv nil state). Thanks to Jared Davis for requesting this change. (Note: this change does not apply if the host Lisp is non-ANSI, i.e., if the host Lisp is non-ANSI GCL.)

The advanced meta-extract mechanisms, provided for using facts from the world or metafunction context, have been enhanced in the following ways, in collaboration with Sol Swords. See meta-extract for more details.

It is now permissible to use calls of meta-extract-global-fact in hypotheses of clause-processor rules, much as they are used in hypotheses of meta rules. See meta-extract. Thanks to Sol Swords for requesting this feature.

The utility meta-extract-global-fact is now a macro, which expands to a corresponding call of the new function, meta-extract-global-fact+. This new function takes an alternate, extra state as an argument; it is not to be executed, and it operates on the alternate state, whose logical world is intended to be the same as that of the ``live'' (usual) state.

A new sort of value for the obj argument is supported for meta-extract-global-fact (and meta-extract-global-fact+), which results in a term equating a function application to its result. See meta-extract, in particular the discussion of :fncall.

It is now possible for trace$ to avoid printing prefixes of the form "n> " and "<n ", while also (optionally) avoiding indentation. See trace$, in particular the discussion of :fmt!. Thanks to Shilpi Goel for requesting this feature.

It was possible for the guard-debug feature to generate duplicate calls of extra-info in hypotheses generated for guard verification. We have eliminated duplicates of this sort.

When in-theory returns without error, it returns a value (:NUMBER-OF-ENABLED-RUNES k), where k is the length of the new current theory. (Formerly, k was returned.) This value is thus printed when an in-theory event is submitted at the top level. Thanks to Gisela Rossi for feedback that led us to make this change.

A new keyword parameter for ld is :ld-missing-input-ok. Its default value is nil, which causes an error, as before, upon failure to open a specified file. Other legal values are t and :WARN; see ld-missing-input-ok and see ld.

Extended *acl2-exports*, in particular adding UNSIGNED-BYTE-P and SIGNED-BYTE-P (thanks to a suggestion by Jared Davis)

Even if the function f is defined to take one or more stobj arguments, the form (ec-call (f ...)) is now legal if all arguments of the call of f are non-stobj objects, in any context where only ordinary object return values are expected.

When the second argument of certify-book is a symbol, that symbol formerly needed to be ? or t, in the "ACL2" package. Now, the symbol-package-name of the second argument is ignored: any symbol whose symbol-name is "?" or "T" is treated the same in that argument position as the symbol ? or t in the "ACL2" package, respectively. Thanks to Warren Hunt and Nathan Wetzler for suggesting consideration of a more relaxed criterion for that second argument.

(For system hackers, not standard ACL2 users:) Utilities initialize-event-user and finalize-event-user now each take a list of three arguments, (ctx body state). Thanks to Harsh Raju Chamarthi for requesting this change.

NEW FEATURES

It is now permissible to specify a stobj field that is itself either a stobj or an array of stobjs. A new primitive, stobj-let, is provided in order to access or update such fields; see stobj-let. Thanks to Warren Hunt and Sol Swords for requesting the ability to specify nested stobjs.

New accessor function (mfc-world mfc) returns the world component of a metafunction context. See extended-metafunctions.

A new xargs keyword, :SPLIT-TYPES, can be used to ``split'' the type declarations from the guard in the following sense. By default, or when :SPLIT-TYPES has value nil, one gets the existing behavior: the terms corresponding to type declarations are conjoined into the guard. However, if :SPLIT-TYPES t is specified, then that is not the case; instead, guard verification will require that these terms are proved under the hypothesis that the guard holds. In this way, one can add type declarations to assist the host Lisp compiler without cluttering the function's guard. See xargs. Thanks to Jared Davis for requesting this feature.

Advanced users may want to see quick-and-dirty-subsumption-replacement-step for a way to turn off a prover heuristic. Thanks to those who have mentioned to us potential issues with this heuristic, most recently Dave Greve.

HEURISTIC IMPROVEMENTS

We made changes to the ``ancestors check'' heuristic (source function ancestors-check-builtin), as follows.

The heuristic could prevent a rewrite rule's hypothesis from being rewritten to true, even when that hypothesis is of the form (force <term>). Now, forcing will take place as expected; see force. Thanks to Robert Krug for bringing this issue to our attention and sending an example, which we include as a comment in the ACL2 source code (see (deflabel note-6-2 ...)).

The heuristic is now delayed until after we check whether the hypothesis is already known, using type-set reasoning alone (in particular, not using rewriting), to be true or to be false. We believe that this is now the ``right'' order for those two operations. We saw a slight speed up in the regression tests (about a percent) with this change, but that might be in the noise.

A technical change makes the heuristic slightly less aggressive in preventing backchaining. Roughly speaking, ordering checks based on function symbol counts could suffice to permit backchaining, where now variable counts also suffice. Thanks to Robert Krug for showing us an example where backchaining led to a term with no free variables that was nevertheless subject to the ancestors check, preventing it from being rewritten.

(For those who use defattach to attach to ancestors-check) We have used defrec to introduce an `ancestor' data structure. A new function, strip-ancestor-literals, should be used to obtain the literals from a list of ancestors, although strip-cars will still work at this time.

When we rewrite the current literal of the current clause we assume the falsity of the other literals and of the conclusions produced by forward chaining. We have changed the order in which those assumptions are made, which affects the type-alist used during rewriting. This has three effects: the new type-alist, which is sometimes stronger than the old one, may allow additional rules to fire, the choice of free vars may be different, and the order of the literals in forced subgoals may be different. Should ``legacy'' proofs fail under the new type-alist, we recommend looking for rules that are fired in the new proof that were not fired (on that same subgoal) in the old one. Thanks to Dave Greve for sending us an example that led us to make this change.

BUG FIXES

We fixed a soundness bug that could be exploited by calling system functions acl2-magic-mfc or acl2-magic-canonical-pathname. Thanks to Sol Swords for bringing this bug to our attention.

We fixed a soundness bug in the handling of stobjs, in which strings were recognized as stobjs in raw Lisp. Thanks to Jared Davis for sending us a proof of nil that exploited this bug. We now have a much simpler example of this bug, as follows.

(defstobj st fld)
(defthm bad (stp "abc") :rule-classes nil)
(defthm contradiction
  nil
  :hints (("Goal" :in-theory (disable (stp)) :use bad))
  :rule-classes nil)

We fixed bugs in extended metafunctions (see extended-metafunctions). The macro mfc-ap no longer takes a :TTREEP keyword argument, because this argument could allow returning a tag tree that does not properly account for forcing. The remaining mfc-xx macros -- mfc-relieve-hyp, mfc-rw+, mfc-rw, and mfc-ts -- still take a :TTREEP keyword argument, but the corresponding functions when :TTREEP is t -- mfc-relieve-hyp-ttree, mfc-rw+-ttree, mfc-rw-ttree, and mfc-ts-ttree -- were introduced with incorrect output signatures. A complication is that mfc-relieve-hyp-ttree was improperly defined in raw Lisp in a way that actually matched the incorrect signature! All of these bugs have been fixed. Perhaps any of them could have made it possible to prove nil, though we have not tried to do so.

(Windows only) On Windows, it had been possible for ACL2 not to consider two pathnames to name the same file when the only difference is the case of the drive, e.g., `C:' vs. `c:'. This has been fixed. Thanks to Sol Swords for reporting this issue.

Fixed a bug in the storing of rules for the tau system; see tau-system. (The error message mentions PARTITION-SIGNATURE-HYPS-INTO-TAU-ALIST-AND-OTHERS.) Thanks to Sol Swords for reporting this bug and sending a simple example to illustrate it.

It had been possible to admit the missing defthm events printed by defabsstobj, and yet get an error when subsequently submitting the same defabsstobj event, stating: ``Note discrepancy with existing formula''. The problem could occur when an expression of the form (or X Y) occurred in one of those missing events, because ACL2 created it from the term (if X 't Y) but then translated (or X Y) to (if X X Y), resulting in a mismatch. This has been fixed. Thanks to Jared Davis for reporting this bug using a simple example.

A hard Lisp error was possible for certain illegal functional substitutions (see lemma-instance). Thanks to Sol Swords for reporting this bug.

We fixed a bug in the case that an exported function of a defabsstobj event had a guard of t. Thanks to Jared Davis for sending a simple example when reporting this bug.

We now avoid an infinite loop that could occur when attempting to close the standard character output channel (see standard-co). Instead, an error message explains how to accomplish what was probably intended. Thanks to Shilpi Goel for bringing this issue to our attention.

(Windows only) Fixed a bug that was causing a hard error on Windows when ACL2 encountered filenames starting with the tilde character (~), for example, (ld "~/acl2-customization.lsp"). Thanks to Sol Swords for bringing this bug to our attention. Also thanks to Harsh Raju Chamarthi for a useful conversation that led to a better fix than our first one.

CHANGES AT THE SYSTEM LEVEL

ACL2 may now be built on recent versions of a new host Lisp, ANSI Gnu Common Lisp (GCL). Traditional (non-ANSI) GCL was the original host Lisp underlying ACL2, and we are grateful for GCL support that we received from the late Bill Schelter and, more recently and particularly for ANSI GCL, from Camm Maguire.

The `make' process suggested for book certification has changed substantially, thanks in large part to contributions from Jared Davis and Sol Swords. We have seen the new process provide better performance on machines with many cores, and we expect maintenance advantages such as eliminating the need for Makefiles in individual book directories. The ``classic'' process, which was based on community books file books/Makefile-generic, is still supported (see books-certification-classic) but may disappear in a future release of ACL2. See books-certification. Most changes should be invisible to the user, other than improved `make'-level parallelism, with the exception of the following.

o Variable ACL2_JOBS is no longer supported, nor is it necessary; simply use `make' option `-j' instead.

o Regressions now use `make' option -k by default, which causes the regression to keep going after errors, rather than -i, which ignores errors. If you encounter problems because of this change, use ACL2_IGNORE=-i with your `make' command.

o The `regression' target works for the experimental extension, ACL2(h) (see hons-and-memoization); target `regression-hons' no longer exists.

Please let us know if you run into problems with the new infrastructure, as we consider the legacy infrastructure to be deprecated and we will probably eliminate much of it in the future. In particular, circular dependencies were formerly prohibited at the directory level, but that is no longer the case, and we expect such cycles to occur in the future.

Although ACL2 users don't typically modify raw Lisp variables, we have arranged to reset Lisp variable *default-pathname-defaults* if necessary at startup so that it will not interfere with ACL2, in particular by messing up the initial connected book directory (see cbd). Thanks to Jared Davis, Sol Swords, and Raymond Toy for helping us to identify this issue.

EMACS SUPPORT

EXPERIMENTAL/ALTERNATE VERSIONS

In ACL2(h), print-object$ no longer uses the serialize printer except in system applications as before (e.g., write out .cert files). Thanks to Dave Greve for bringing this issue to our attention.

Jared Davis contributed changes related to the memoize utility of ACL2(h), including some low-level changes as well as the following.

o Never-memoize specifies that a given function should never be memoized.

o Removed memoize-let, which may never have ever been used.

o Removed the :inline keyword option to memoize, which was just an alias for the :recursive option.

For ACL2(p), some anomalous behavior may no longer occur because prover calls (more specifically, trips through the ACL2 ``waterfall'') will return only after all sub-computations (threads) have finished. Thanks to David Rager for contributing this improvement.

ACL2(pr), which includes parallelism (as for ACL2(p)) and non-standard analysis support for the reals (as for ACL2(r)), now builds and can certify the community nonstd/ books. Thanks to David Rager for his contribution to this capability.