NOTE-2-9

ACL2 Version 2.9 (October, 2004) Notes 
Major Section:  RELEASE-NOTES


TABLE OF CONTENTS.


==============================
BUG FIXES.
NEW FUNCTIONALITY.
CHANGES IN PROOF ENGINE.
GUARD-RELATED CHANGES.
PROOF-CHECKER CHANGES.
SYSTEM-LEVEL CHANGES.
BOOK CHANGES.
MISCELLANEOUS CHANGES.
==============================

BUG FIXES.

We fixed a soundness bug due to a conflict between user-supplied package names and internal package names (obtained by prepending a Lisp constant, *1*-package-prefix*) and user-supplied package names. For example, the form (defpkg "ACL2_*1*_MYPKG" ()) is no longer legal. Thanks to Robert Krug for asking a question that led directly to the discovery of this bug.

We fixed a soundness bug that allows :logic mode functions to call :program mode functions. The fix furthermore prevents functions with guards verified from calling functions with guards not verified. We had thought we already prevented all this, but there was a problem with the interaction of local definitions and redundancy checking (see redundant-events).

We fixed a soundness bug that could occur when built-in functions were called during macroexpansion (a hole in so-called ``safe-mode'').

Fixed a minor bug in system functions genvar1 and genvar, where eq had been used in place of eql. This bug was discovered during the plugging of a hole in safe-mode, mentioned just above.

We fixed handling of the :inline keyword for defstobj, which previously could cause raw Lisp errors in OpenMCL and CMU Common Lisp. Thanks to John Matthews for bringing this issue to our attention.

Calls of include-book could result in a state for which some function definitions were not compiled that should have been. The result could be performance degradation or even stack overflows. This situation could arise in the following two ways.

o Inclusion of a book with an absolute pathname that differs from the absolute pathname at certification time, presumably because of the use of soft links. Thanks to Bob Boyer and Warren Hunt for bringing a stack overflow to our attention that led us to this fix.

o Large mutual-recursion nests (more than 20 functions) are executed in a superior book.

We fixed some performance bugs that can increase the speed of include-book calls by a factor of close to 2. Thanks to Eric Smith for asking if we could speed up include-book processing; we have done so in the past, but primarily focusing on large mutual-recursion nests (which have nothing in particular to do with the current improvements). Also, thanks to Rob Sumners for a very useful remark early in the process that kept us from drawing an incorrect conclusion at that point.

We fixed :pl so that it can be run on a form that returns multiple values, which it could not do previouslly. Thanks to Eric Smith for pointing out this problem.

Fixed a bug in the Allegro ACL2 trace utility (see trace$) that was causing ``10>'' to be printed as ``9>'', ``11>'' to be printed as ``10 >'', ``12>'' to be printed as ``11 >'', and so on.

Fixed a proof-checker bug that was preventing the use of the DV command (or a numerical command) on let expressions. Thanks to Bill Young for pointing out this problem.

Fixed a bug in a comment on how to set ACL2_BOOKS_DIR in the makefile. Thanks to Dave Greve for pointing out this problem.

Fixed a potential soundness bug in the linear arithmetic routines. Thanks to Jared Davis for noticing this problem and to Robert Krug for implementing the fix. (Technical details: We had been assuming that polynomials were being normalized -- see the definition of good-polyp in linear-a.lisp -- but this assumption was false.)

When the macro open-trace-file is opened twice in succession, it now automatically closes the first trace output channel before opening another.

It is now possible to use make to build ACL2 on Windows systems that support make. Thanks to Pete Manolios and Mike Thomas for pointing out the problem, to Jared Davis and Mike for helping us to analyze the problem, and to Jared for testing the fix.

Fixed a bug in the guard of with-output that was causing a needless guard violation.

NEW FUNCTIONALITY.

The new events add-default-hints and remove-default-hints allow one to append to or subtract from the current list of default hints. The event set-default-hints continues to set the list of default hints, discarding the previous value of the default-hints. Note that set-default-hints is still local to the encapsulate or book in which it occurs, and add-default-hints has the same property, although neither is implemented any longer using the acl2-defaults-table. New events add-default-hints!, remove-default-hints!, and set-default-hints! are the same as add-default-hints, remove-default-hints, and set-default-hints, respectively, except that the former three events are not local to their enclosing encapsulate or book. Thanks to Jared Davis for suggesting these enhancements.

OpenMCL's tracing routines have been modified in a similar manner as those of Allegro CL. Thanks to Robert Krug for providing this enhancement.

Guard-checking can now be caused to happen on recursive calls. See ``GUARD-RELATED CHANGES'' below for details.

Advanced users can now inhibit compilation of so-called ``*1* functions'' with the :comp command; see comp. Thanks to Rob Sumners for suggesting this enhancement.

Added new legal argument hard? for the er macro, which is now documented. See er. Thanks to Rob Sumners for a discussion leading to this change. Also, the three legal first arguments to er -- hard, hard?, and soft -- may now be in any package (thanks to Jared Davis for bringing this issue to our attention).

We have removed the requirement that for a rule's hypothesis (bind-free term var-list), at least one variable must occur free in term. For example, the expression (bind-free (bind-divisor a b) (x)) was legal because a and b occur free in (bind-divisor a b); but (bind-free (foo (bar)) (x)) was not legal. The latter is no longer disallowed. (Technical note: this allows bind-free to be used to create explicit substitutions in metafunction hypotheses.)

The following two enhancements have been implemented for rules of class :meta. Thanks to Eric Smith for requesting more control of reasoning with :meta rules, which led to these enhancements, and to him and Robert Krug for helpful discussions.

o It is now possible to control backchaining in rules of class :meta by providing a :backchain-limit-lst argument, as was already allowed for rules of class :rewrite and :linear. See rule-classes. However, unlike those other two rule classes, the value for :backchain-limit-lst is prohibited from being a non-empty list; it must be either nil or a non-negative integer.

o (For advanced users.) It is now legal for hypothesis metafunctions to generate, in essense, calls of syntaxp and bind-free, handled essentially as they are handled in hypotheses of :rewrite and :linear rules. We say ``essentially'' primarily because both syntaxp and bind-free are actually macros, but hypothesis metafunctions must generate translated terms (see term). The enterprising advanced user can call :trans to see examples of translated terms corresponding to calls of syntaxp and bind-free.

A new command :trans! has been added, which is like :trans except that :trans! ignored issues of single-threadedness. See trans!. Thanks to Eric Smith for suggesting this addition.

The :pf command now works when the argument is the name of a macro associated with a function by macro-aliases-table.

CHANGES IN PROOF ENGINE.

The simplifier has been changed slightly in order to avoid using forward-chaining facts derived from a literal (essentially, a top-level hypothesis or conclusion) that has been rewritten. As a practical matter, this may mean that the user should not expect forward-chaining to take place on a term that can be rewritten for any reason (generally function expansion or application of rewrite rules). Formerly, the restriction was less severe: forward-chaining facts from a hypothesis could be used as long as the hypothesis was not rewritten to t. Thanks to Art Flatau for providing an example that led us to make this change; see the comments in source function rewrite-clause for details.

The rewriter has been modified to work slightly harder in relieving hypotheses. Thanks to Eric Smith for providing an example that inspired the following, which illustrates the issue. Suppose we introduce functions foo and bar with the (non-local) properties shown below. 

 (encapsulate
  (((foo *) => *)
   ((bar *) => *))


  (local (defun foo (x) (declare (ignore x)) t))
  (local (defun bar (x) (declare (ignore x)) t))


  (defthm foo-holds
    (implies x
             (equal (foo x) t)))
  (defthm bar-holds-propositionally
    (iff (bar x) t)))
Consider what happens when ACL2's rewriter is used to prove the following theorem. 
(thm (foo (bar y)))
With ACL2's inside-out rewriting, (bar y) is first considered, but rewrite rule bar-holds-propositionally does not apply because the context requires preserving equality, not mere Boolean (iff) equivalence. Then the rewriter moves its attention outward and sees the term (foo (bar y)). It attempts to apply the rule foo-holds, in a context created by binding its variable x to the term (bar y). It then attempts to relieve the hypothesis x of rule foo-holds in that context. Before this change, ACL2 basically assumed that since rewriting was inside out, then (bar y) had already been rewritten as much as possible, so the rewrite of x in the aforementioned context (binding x to (bar y)) simply returned (bar y), and the attempt to relieve the hypothesis of foo-holds failed. The change is essentially for ACL2's rewriter to make a second pass through the rewriter when the attempt fails to rewrite a variable to t, this time using the fact that we are in a Boolean context. (We mention that source function rewrite-solidify-plus implements this idea, for those who want to dig deeply into this issue.) In our example, that means that the rewriter considers (bar y) in a Boolean context, where it may apply the rule bar-holds-propositionally to relieve the hypothesis successfully.

When (set-non-linearp t) has been executed, non-linear-arithmetic can now be applied in some cases for which it previously was not. Thanks to Robert Krug for supplying this modification and to Julien Schmaltz for providing a motivating example.

We modified the rewriter to avoid certain infinite loops caused by an interaction of the opening of recursive functions with equality reasoning. (This change is documented in detail in the source code, in particular functions rewrite-fncall and fnstack-term-member.) Thanks to Fares Fraij for sending us an example that led us to make this change.

The :executable-counterpart of function hide is now disabled when ACL2 starts up. This removes an anomoly, for example that 

(thm (not (equal 1 (* (hide 0) a))))
succeeded while 
(thm (equal (foo (equal 1 (* (hide 0) a))) (foo nil)))
failed. Now both fail.

The theory *s-prop-theory* is no longer used by the proof-checker; it has been replaced by (theory 'minimal-theory. We have left the constant *s-prop-theory* defined in the source code in support of existing books, however. This change eliminates annoying theory warnings printed upon invocation of proof-checker commands s-prop, sl, and split.

Terms are now kept in an internal form that avoids calls of primitive functions (built-ins without explicit definitions; see code for cons-term for details), in favor of the constants that result from evlaluating those calls. So for example, the internal form for (cons 1 2) is (quote (1 . 2)). This change was made at around the same time as changes in support of bind-free; see above. One consequence is that the splitting of goals into cases (technically, source function clausify and even more technically, source function call-stack) has been modified, which can cause subgoal numbers to change.

GUARD-RELATED CHANGES.

Guard-checking can now be caused to happen on recursive calls, where this was formerly not the case for :program mode functions and, perhaps more important, for :logic mode functions whose guards have not been verified. Moreover, a warning is printed when ACL2 does not rule out the exclusion of guard-checking on recursive calls. See set-guard-checking. Thanks to David Rager for bringing this issue to our attention, and to Rob Sumners and the Univ. of Texas ACL2 seminar in general for their feedback.

Guard violations are reported with less of the offending term hidden. Thanks to Jared Davis for suggesting that we look at this issue.

PROOF-CHECKER CHANGES.

We fixed the proof-checker so that diving works as you might expect for a macro call (op a b c) representing (binary-op a (binary-op b c)). In the past, if the current term was of the form (append t1 t2 t3), then (DV 3) (and 3) would dive to t3 even though the corresponding function call is (binary-append t1 (binary-append t2 t3)). This is still the case, but now this behavior holds for any macro associated with a function in binop-table (see add-binop). Moreover, users can now write customized diving functions; see dive-into-macros-table, and also see books/misc/rtl-untranslate.lisp for example calls to add-dive-into-macro. Of course, the old behavior can still be obtained using the proof-checker's DIVE command; see proof-checker-commands.

The runes command in the proof-checker now shows only the runes used by the most recent primitive or macro command (as shown by :comm), unless it is given a non-nil argument. Also, proof-checker command lemmas-used has been added as, in essence, an alias for runes.

(The following two items are also mentioned above under ``BUG FIXES.'')

Fixed a proof-checker bug that was preventing the use of the DV command (or a numerical command) on let expressions. Thanks to Bill Young for pointing out this problem.

The theory *s-prop-theory* is no longer used by the proof-checker; it has been replaced by (theory 'minimal-theory. We have left the constant *s-prop-theory* defined in the source code in support of existing books, however. This change eliminates annoying theory warnings printed upon invocation of proof-checker commands s-prop, sl, and split.

SYSTEM-LEVEL CHANGES.

Fixed a problem with building ACL2 on CMUCL in some systems (source function save-acl2-in-cmulisp). Thanks to Bill Pase for bringing this to our attention.

The installation instructions have been extended to include instructions for building on GCL in Mac OS X. Thanks to Jun Sawada and Camm Maguire.

Initial pre-allocation of space has been updated for GCL to reflect more current GCL executables (we considered GCL 2.6.1-38). This can help avoid running out of memory for large ACL2 sessions.

The main Makefile has been replaced by GNUmakefile, in order to enforce the use of GNU make. If you use another make program, you'll get an error message that may help you proceed.

(GCL only) SGC is no longer turned on for GCL 2.6 sub-versions through 2.6.3 if si::*optimize-maximum-pages* is bound to T, due to an apparent issue with their interaction in those sub-versions. Also, we have eliminated preallocation for all versions after 2.6.1 because GCL doesn't need it (comments are in source function save-acl2-in-akcl). Thanks to Camm Maguire for excellent GCL help and guidance, and to Camm and Bob Boyer for useful discussions.

We have removed support for so-called ``small'' images. Thus, :doc, :pe and :pc, verify-termination, and other commands are fully supported in ACL2 saved images. Because of this and other changes in the generation of the so-called ``*1*'' logical functions, related to guards (as described above in -GUARD-RELATED CHANGES'', and related to the discussion of safe-mode in ``BUG FIXES'' above), image sizes have increased substantially.

We no longer time or run ``nice'' the certification of individual books. The file books/Makefile-generic had done these by default, and some individual distributed and workshop book directories had Makefiles that did so as well. Thanks to Mike Thomas, who pointed out the lack of nice on some Windows systems (and we decided on this simple solution). Overall targets in books/Makefile still time their runs by default, and the partiular time program is now controlled by a Makefile variable.

Failures during make certify-books or make regression now show up in the log as ``**CERTIFICATION FAILED**'', regardless of the operating system (as long as it supports make). Formerly, one searched for ``**'' but this did not appear in openMCL runs.

We have eliminated ``Undefined function'' warnings that could occur in OpenMCL.

BOOK CHANGES.

Reconciled the definitions of firstn in book/misc/csort.lisp, books/bdd/bdd-primitives.lisp, books/ordinals/ordinal-definitions.lisp, and books/data-structures/list-defuns.lisp. Thanks to Ray Richards for bringing this issue to our attention.

Distributed book books/misc/defpun now can handle stobjs where it did not previously. Thanks to John Matthews for bringing this issue to our attention.

The "make" variable COMPILE_FLG in file books/Makefile-generic formerly only had an effect if there was a cert.acl2 file present. That oversight has been remedied.

File "books/arithmetic/certify.lsp" was missing a certify-book command for "natp-posp". Thanks to John Cowles for noticing this deficiency and supplying a fix. (This file is of use to those who want to certify the "books/arithmetic/" books without using "make".)

A few small changes have been made to "books/rtl/rel4".

Small changes were made to books misc/symbol-btree and misc/rtl-untranslate. In particular, the definition of symbol-btreep was strengthened.

We made a minor fix to books/ordinals/e0-ordinal.lisp, adding (verify-guards ob+) and hence (verify-guards ocmp) as well. This was necessitated by the fix prohibiting functions with guards verified from calling functions with guards not verified (see also the related discussion under ``BUG FIXES'' above).

MISCELLANEOUS CHANGES.

Further sped up processing of large mutual-recursion nests (extending what was done for Version_2.7), perhaps by a factor of two in some cases.

As promised in Version_2.5 (see note-2-5), structured pathnames are no longer supported. So for example, the argument to include-book must now be a string constant.

Some documentation has been improved, for stobjs thanks to suggestions by John Matthews and much of the rest thanks to feedback from Eric Smith.

The function current-package is now available to users (it has been taken off the list of so-called ``untouchables''). Thanks to Jared Davis for bringing this issue to our attention.

The documentation for topic using-computed-hints-7 has been improved. Thanks to Doug Harper and Eric Smith for inspiring this improvement.

We added several symbols to *acl2-exports*: cw, er, intern$, set-case-split-limitations, and set-difference-eq. Thanks to Jared Davis for suggesting most of these.

Now, a table event that sets the value for a key, (table tbl key val :put), is redundant (see redundant-events) when it does not change the value associated with an existing key of the table. In particular, define-pc-macro is now fully redundant when it does not change an existing proof-checker macro-command definition. Thanks to Bill Young for bringing the latter issue to our attention.

The definitions of unused system functions ev-w and ev-w-lst have been deleted.

ACL2 now prints a warning if a defpkg event introduces a package name with lower-case letters, since there is opportunity for later confusion in that case. Thanks to Frederic Peschanski for bringing this problem to our attention and Sandip Ray for encouragement.

ACL2 now works in Version 19 of CMU Common Lisp.

The function sys-call has been modified so that for ACL2 built on Allegro Common Lisp in Unix or Linux, the existing environment is used. Thanks to Erik Reeber for bringing this issue to our attention.

The function disabledp can now be given a macro name that has a corresponding function; see macro-aliases-table. Also, disabledp now has a guard of t but causes a hard error on an inappropriate argument.