Note-2-9
ACL2 Version 2.9 (October, 2004) Notes
Table of Contents
- BUG FIXES
- NEW FUNCTIONALITY
- CHANGES IN PROOF ENGINE
- GUARD-RELATED CHANGES
- PROOF-BUILDER 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 previously. 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-builder 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 essence, 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 anomaly, 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-builder; 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-builder
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 evaluating 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-BUILDER CHANGES.
We fixed the proof-builder 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-builder's DIVE command; see proof-builder-commands.
The runes command in the proof-builder 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-builder 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-builder 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-builder; 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-builder
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 particular 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-builder 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.
