Major Section: RELEASE-NOTES
This is the first version of ACL2 released under the copyright of the University of Texas (UT). Future releases of ACL2 will be made from UT rather than Computational Logic, Inc. (CLI). Version 2.0 is just Version 1.9 as released by CLI, with a few bugs fixed.
A bug causing an infinite loop was fixed in functional instantiation.
The bug manifested itself when two conditions occurred simultaneously:
First, the functional substitution replaces a function symbol, e.g., FOO,
with a LAMBDA expression containing a free variable (a variable not among
in the LAMBDA formals). And, second, in one of the constraints being
instantiated there is a call of the function symbol FOO within the scope
of another LAMBDA expression. Unless you used such a functional
substitution, this bug fix will not affect you.
Less important notes:
The implementation of PRINC$ was changed so that it was no longer
sensitive to the external setting of *print-base* and other Common Lisp
special variables.
Typographical errors were fixed in the documentation.
Major Section: RELEASE-NOTES
The identity function case-split has been added. It is similar
to force but causes an immediate split of the top-level goal on
whether the indicated hypothesis is true.
Less important notes:
Minor bugs in the documentation were fixed.
Major Section: RELEASE-NOTES
Important changes:
A bug was fixed in the compile command, :comp. The compiled code
produced by :comp in previous versions could be wildly incorrect
because of a confusion between the printer and the reader regarding
what was the current Lisp *package*. This bug could manifest itself
only if you used the :comp command to compile previously uncompiled
functions while the current package was different from "ACL2".
What happened in that situation depended upon what symbols were
imported into your current package. The most likely behavior is
that the compiler would break or complain or the resulting compiled
code would call functions that did not exist.
There have been no other important changes to the code.
However, this release contains some useful new books, notably those on
the books subdirectories cli-misc and ihs. Both have
README files. The ihs books provide support for integer
hardware specifications. These books were crucial to Bishop Brock's
successful modeling of the Motorola CAP. We thank Bishop for producing
them and we thank all those who worked so hard to get these books released.
We highly recommend the ihs books to those modeling ALUs and other
arithmetic components of microprocessors or programming languages.
In previous versions of ACL2, the arithmetic books, found on
books/arithmetic/, included the addition of several unproved axioms
stating properties of the rationals that we believed could be derived from
our ``official'' axioms but which we had not mechanically proved. The axioms
were found in the book rationals-with-axioms.lisp,
which was then used in the uppermost arithmetic books top.lisp and
top-with-meta.lisp. John Cowles has now provided us with ACL2 proofs
of those ``axioms'' and so in this release you will find both
rationals-with-axioms.lisp and rationals-with-axioms-proved.lisp.
The former is provided for compatibility's sake. The latter is identical
but contains defthms where the former contains defaxioms.
The top-most books have been rebuilt using ``-axioms-proved'' book.
Thanks John.
Less important notes:
Bishop Brock found a bug in translated-acl2-unwind-protectp4.
Jun Sawada reported a bug in linear arithmetic that caused us not to
prove certain trivial theorems concluding with (not (equal i j)).
We have fixed both.
We now prohibit definitions that call certain event commands
such as DEFTHM and TABLE because our Common Lisp implementations
of them differ from their ACL2 meanings (so that compiled books
can be loaded correctly and efficiently).
Minor bugs in the documentation were fixed.
Major Section: RELEASE-NOTES
Important changes:
Versions of ACL2 preceding this one contain a subtle soundness bug! We found a flaw in our detection of subversive-recursions. The bug allowed some subversive recursions to slip through undetected.
We believe it would have been difficult to have exploited this flaw
inadvertently. In particular, the following five conditions are
necessary.
(1) Introduce a constrained function, say f, via an encapsulate.
(2) In the same encapsulation, define a clique of mutually
recursive functions. This clique must be non-local and in
:logic mode.
(3) In that mutually recursive clique, use the constrained function
f (perhaps indirectly) so that the termination argument for the
clique depends on properties of the witness for f. Thus,
f or some other function dependent upon f, must be used in
an argument in a recursive call or in a term governing a recursive
call. Furthermore, the use of f must be such that the
termination proof cannot be done without exploiting properties of
the witness for f. Other uses of the constrained functions in
the clique are ok.
(4) Fail to include the exploited properties of f among the
constraints of the encapsulation.
(5) Later, outside the encapsulation, explicitly use a functional
instantiation in which f is replaced by a function not enjoying
the crucial properties.
See subversive-recursions for details.
Less important notes:
We have begun to write some introductory tutorial material for those
who wish to learn to program in ACL2. Most of this material is
HTML-based. See the Hyper-Card on the ACL2 home page.
The documentation of verify-guards was improved to explain why
one might wish to verify the ``guards'' of a defthm event. The
missing documentation was noticed by John Cowles.
A bug was fixed in cross fertilization. The bug caused the system to report that it had substituted one term for another when in fact no substitution occurred. The bug was noticed by Bill McCune.
Major Section: RELEASE-NOTES
Important changes:
We corrected a soundness bug in Version 2.3 related to the handling of
immediate-force-modep. The bad behavior was noticed by Robert
Krug. Thanks!
We corrected a bug that permitted verify-guards to accept a function
even though a subfunction had not yet had its guards verified. Thanks to
John Cowles for noticing this.
User defined single-threaded objects are now supported. See stobj.
Less important notes:
We corrected a bug that prevented the intended expansion of some recursive function calls.
We changed the handling of the primitive function ILLEGAL, which
is logically defined to be nil but which is programmed to signal an
error, so that when it is evaluated as part of a proof, it does not signal
an error. The old handling of the function prevented some guard proofs
involving THE or LETs with internal declarations.
We corrected a bug that permitted some LOCAL DEFAXIOM events to slip
into certified books.
We corrected a bug that prevented the correct undoing of certain DEFPKG
forms.
Changes were made to support CMU Lisp. Pete Manolios helped with these changes.
Changes were made to make the make files more compatible with Allegro Common Lisp. Jun Sawada, who has been a great help with keeping ACL2 up and running at UT on various platforms, was especially helpful. Thanks Jun.
Major Section: RELEASE-NOTES
Important Changes:
Concurrent with the release of ACL2 Version 2.5 is the publication of two books about ACL2. See the ``Books and Papers about ACL2 and Its Applications'' on the ACL2 Home Page.
The books subdirectory now contains many new certifiable books,
including solutions to the exercises in the two published books and
full scripts for the case studies. See books/README.html.
Improved Unix Makefile support for book certification has also been
written. See books/README.html.
The list of symbols in *acl2-exports* has been considerably expanded.
If you have packages built by importing *acl2-exports* you might want
to look carefully at the new value of that constant. The new value includes
all :logic mode functions as of Version 2.5, as well as all documented
macros and all built-in theorem names.
Include-book and certify-book were modified to
have some additional keyword arguments. It is possible to
certify a book containing defaxiom and/or skip-proofs
events and get warning messages or errors signaled, according to
the settings of these new flags. In addition, it is possible to
specify in include-book whether the book must be certified
(under penalty of error if not). The default values of these new
arguments cause warnings to be printed rather than errors signaled.
The above change involved altering the form of certificate files.
When books certified under previous versions are included, more
warnings will be generated because these books are considered
possibly to contain defaxiom and/or skip-proofs events.
We anticipate further changes to this aspect of books and consider the current mechanisms (for controlling whether warnings or errors are signaled) just a prototype. See also the discussion below of ``soundness related'' warnings. Your suggestions are welcome.
A discrepancy between ACL2 and Common Lisp was fixed, having to do
with declare ignore. In past versions of ACL2, a formal
parameter of a defun was considered ignored if it was not used
in the body, the guard or the measure of the defun. That meant
that a variable used only in the guard could not be declared ignored
in ACL2; but some Common Lisp compilers would complain because the
variable was not used in the body. Now, ACL2 considers a variable
ignored if it is not used in the body.
ACL2 can now be built in releases 5.0 and later of Allegro Common Lisp. (Other releases of Allegro Common Lisp and of other lisps continue to be supported as well.) This includes Allegro Common Lisp running on Windows 98 platforms. John Cowles helped us do some testing and answered questions for us. Thanks John!
We incorporated Ruben Gamboa's changes to allow the building of a variant, ACL2(r), of ACL2, in which the user can reason about the real numbers using non-standard analysis. See real. Note that ACL2(r) and ACL2 have different underlying theories, and books certified in one system may not be included in the other. For backward compatibility and to ensure a smooth transition, ACL2 is built by default, not ACL2(r). This is a compile-time switch; see the makefile for instructions. There should be no changes to ACL2 resulting from the capability of building ACL2(r) from the same sources. Also see acknowledgments for more on the history of ACL2(r).
A large number of bugs (some affecting soundness) were fixed, and many small new features were added. See below.
Less Important Changes:
Some warnings are now considered ``soundness related,'' namely,
those that advise you that an uncertified book has been included
or that a book containing DEFAXIOM or SKIP-PROOFS events.
(Technically, DEFAXIOMs do not imperil soundness in the proof-
theoretic sense, though they may imperil the validity of theorems.
But you sould know when a book has added an axiom to your logic!) In
previous versions of ACL2, all warnings were inhibited if the token
warning was included in the argument to
set-inhibit-output-lst. Now, soundness related warnings are
printed even if warnings have been inhibited. To inhibit all
warnings, supply the token warning! to set-inhibit-output-lst.
Several bugs in defstobj were fixed, relating to the
possibility that some of the subfunctions introduced by the
defstobj were already defined.
:Puff no longer tries to expand defstobj events.
Previously, the attempt would cause a hard error.
A soundness bug was fixed. The bug might have been exercised if you
had an alternative definition (implies hyps (equiv (fn ...) body)) in
which equiv is an equivalence relation other than EQUAL. In this case,
calls of fn might have been expanded to body in places that were not
equiv-hittable.
An obscure soundness bug was fixed. The bug was exercised only if you had a metafunction with a computed hypothesis (i.e., a ``meta hypothesis function''), the hypothesis contained a free variable, i.e., a variable not involved in the term being rewritten, and the free variable occurred in the output of the metafunction. The possibility of this bug was brought to our attention by Robert Krug.
We fixed a bug in the handling of hide related to the question
of whether a variable symbol occurs in a term. The old code did not
find the variable and could cause the system to throw away a
hypothesis about it on the grounds that it was never mentioned. Rob
Sumners helped discover this problem.
The handling of :elim rules was generalized, permitting arbitrary
known equivalence relations instead of merely equal in the
concluding equality.
The printing of runes (rule names; see rune) used has been made "deterministic," both in proof output and in proof attempt summaries, by sorting the runes before printing.
The handling of free variables has been improved for hypotheses such
as (< 0 X), and more generally, any hypotheses involving a
comparison with 0 (even for example (< X 1) where X is known to be
an integer, which is handled as (<= X 0)). Thanks to Robert Krug
for bringing relevant examples to our attention.
A new value, :comp, has been implemented for the
:load-compiled-file keyword of include-book. If this
value is supplied, then a compiled file will always be loaded, even
if that requires creating the compiled file first.
The event include-book now generates a warning when a compiled
file is expected but not found (see include-book). Formerly,
it only did so when executed at the top level; it failed to generate
the warning when executed on behalf of a surrounding include-book
command.
Certain redefinition warnings generated by Allegro Common Lisp have been eliminated.
A new key has been implemented for the acl2-defaults-table,
:bogus-mutual-recursion-ok, set with :set-bogus-mutual-recursion-ok.
Thanks to David Russinoff for pointing out the utility of such a key.
A bug was fixed in defun-sk that prevented its generated events from
being accepted when guard verification is being performed. Thanks
to Bill Young for bringing this problem to our attention. A second
bug was brought to our attention by Pete Manolios, which was causing
certain defun-sk events to be rejected. That problem has been
fixed, and an "Infected" warning has also been eliminated.
The command good-bye now works with Allegro Common Lisp.
A low-level bug was fixed that could, for example, cause an error
such as "Error: Expected 5 args but received 4 args" when
interrupting a local event.
A bug has been fixed in the proof-checker related to definition expansion. Thanks to Pete Manolios for bringing this to our attention with a simple example.
A bug has been fixed related to the :bdd hint in the presence of
equivalence relations. Thanks to Pete Manolios for bringing this to our
attention with a simple example.
The functions position and position-equal formerly
required the second argument to be a true list. In accordance with
Common Lisp, we now also allow the second argument to be a string.
This could cause earlier proofs about these functions to fail unless
true-listp is known to hold where necessary.
Robert Krug wrote a patch, which has been incorporated, to prevent certain infinite loops that can arise in linear arithmetic. Thanks, Robert!
The macro let* no longer requires the bound variables to be
distinct.
An obscure bug was fixed related to congruence rules. The bug would sometimes cause ACL2 to behave as though no rules (other than equality) were available for some argument positions. Thanks to Pete Manolios for bringing this bug to our attention.
Documentation topics have been added for hard-error and prog2$,
and the documentation for illegal has been improved. Thanks to Rob
Sumners for a useful suggestion in the examples in documentation for
prog2$ and a fix in documentation for sublis.
The event form certify-book was made more secure, in that it can now
catch attempts to write a book to disk during its certification.
Thanks to Rob Sumners for pointing out the insecurity of the
existing mechanism.
A Y2K problem was fixed with our applicative handling of dates.
Accessors and updaters for stobjs have been made more efficient when
the underlying lisp is Allegro Common Lisp, by the use of
appropriate simple array declarations.
A raw Lisp break had been possible when a certified book that had no
guard verification was included in a session after
(set-verify-guards-eagerness 2). This has been fixed.
The keyword command :comp can now be used to compile only raw
Lisp functions, excluding executable counterparts, by supplying the
argument :raw.
Rewrite rule nth-of-character-listp was removed from source file
axioms.lisp since it is essentially subsumed by characterp-nth.
Printing has been sped up. In one example the improvement was over 50% in both Allegro and GCL.
We now allow printing in a "downcase" mode, where symbols are
printed in lower case. All printing functions except print-object$
now print characters in lower case for a symbol when the ACL2 state
global variable print-case has value :downcase and vertical bars are
not necessary for printing that symbol. See IO for a discussion of
the macros acl2-print-case and set-acl2-print-case. The default
printing remains unchanged, i.e., symbols are printed in upper case
when vertical bars are not required.
A low-level printing function (prin1$) was modified so that it is
not sensitive to various Common Lisp globals related to printing. So
for example, the function fmt is no longer sensitive to the value
of Common Lisp global *print-case*. (The preceding paragraph
explains how to control the case for printing in ACL2.)
The definition of array1p was fixed so that the :maximum-length of
an array must be strictly greater than the number specified in the
:dimensions field; they may no longer be equal. This was always the
intention; the documentation (see arrays) has remained unchanged.
The corresponding change was also made to array2p. Allegro Common
Lisp formerly caused an error when compress1 was called on an array
where the numbers above were equal; now, we get a guard violation
instead, which is appropriate.
In the context of theories, a name now represents not just the
corresponding :definition rune, as it has done in earlier versions
of ACL2, but also the corresponding :induction rune.
See theories for a discussion of runic designators. Most users
will rarely, if ever, notice this change. One situation where this
change will make a difference is after executing
(in-theory (current-theory 'foo)) followed by
(in-theory (enable bar)), where function bar is introduced after
event foo, and bar is recursively defined. The latter in-theory
form now enables the rune (:induction bar), which implies that the
prover can use the induction scheme stored at definition time for
bar. Formerly, the rune (:induction bar) was not enabled by
(in-theory (enable bar)), and hence the induction scheme for bar was
ignored even when explicit :induct hints were supplied.
You may now supply xargs keyword pair :normalize nil in order to
prevent certain definitions from ``hanging'' when there are many
if-subexpressions. see defun.
We now translate type declarations of real into guards, as we have
already done for other types such as rational. For example,
(declare (type real x)) generates the guard (rationalp x).
See type-spec.
The theorem prover now behaves reasonably under the combination of
specifying a value of t both for :otf-flg and for a hint
:do-not-induct. Previously, it aborted the first time it would have
otherwise pushed a goal for induction, but now, it will continue and
wait until all induction subgoals have been pushed before it aborts.
We changed slightly the definition of round. However, we believe
that the new definition is equivalent to the old.
The definition of Common Lisp function substitute has been added.
The following changes have been made in the use of file names within ACL2. We thank Warren Hunt and John Cowles for running some tests of these changes on Macintosh and Windows 98 platforms (respectively).
It is no longer necessary to issue(1) Names of directories and files now use a syntax like that used for Unix (trademark of AT&T), where directories are separated using the ``
/'' character even when the operating system is not Unix or Linux. See pathname. ACL2 also continues to support its notion of structured pathnames from Version 2.4 and before, but might not do so in future releases and hence no longer documents such syntax.(2) The command
:set-cbdmay now take a relative pathname as an argument.(3) When the macro
ldis given a file name as a value forstandard-oi, then if that file name is a relative pathname it refers to the result of prepending the connected book directory (see pathname, see cbd, and see set-cbd) in order to obtain an absolute pathname. Simiarly for theldspecialsstandard-coandproofs-co.
:set-state-ok t if you
include a stobj declaration for state, for example:
(declare (xargs :stobjs state))See declare-stobjs.
The proof-checker has been cleaned up a bit, including the documentation and the capability (once again) to define pc-macro commands (see define-pc-macro) and proof-checker meta commands (see define-pc-meta).
Recall that events generate summaries that include a line beginning
with ``Warnings:'', which is followed (on the same line) by zero or
more brief strings that summarize the warnings generated by that
event. Formerly, this warnings summary for an encapsulate or
include-book event did not include the summary strings for
warnings generated by subsidiary events. This has been fixed.
Macro cw has been documented and now expands to a call of
a ;logic mode function. See cw for a way to print to the screen
without having to involve the ACL2 state. Thanks to Rob Sumners
for suggesting that we document this useful utility.
Functions duplicates, add-to-set-equal, intersection-eq, evens, and
odds are now :logic mode functions.
Major Section: RELEASE-NOTES
The new features are extensively documented. The relevant topics are:
:doc or :more-doc's ``(cont'd)''
:more
keyword command is so handy for reading long documentation strings
that we recommend you start with :doc more if reading at the
terminal. Some documentation has been written for guards which
you might find interesting.
Major Section: RELEASE-NOTES
Hacker mode has been eliminated and programming mode has been added.
Programming mode is unsound but does syntax checking and permits
redefinitions of names. See :doc load-mode and :doc g-mode.
The arguments to ld have changed. Ld is now much more
sophisticated. See ld.
For those occasions on which you wish to look at a large list
structure that you are afraid to print, try (walkabout x state),
where x is an Acl2 expression that evaluates to the structure in
question. I am afraid there is no documentation yet, but it is
similar in spirit to the Interlisp structure editor. You are
standing on an object and commands move you around in it. E.g., 1
moves you to its first element, 2 to its second, etc.; 0 moves you
up to its parent; nx and bk move you to its next sibling and
previous sibling; pp prettyprints it; q exits returning nil; = exits
returning the thing you're standing on; (= symb) assigns the thing
you're standing on to the state global variable symb.
Several new hints have been implemented, including :by and :do-not.
The old :do-not-generalize has been scrapped in favor of such new
hints as :do-not (generalize elim). :By lets you say ``this goal is
subsumed by'' a given lemma instance. The :by hint also lets you
say ``this goal can't be proved yet but skip it and see how the rest
of the proof goes.'' See hints.
Major Section: RELEASE-NOTES
Programming mode has been eliminated. Instead, all functions have a
``color'' which indicates what can be done with the function. For
example, :red functions can be executed but have no axioms
describing them. Thus, :red functions can be introduced after
passing a simple syntactic check and they can be redefined without
undoing. But nothing of consequence can be proved about them. At
the other extreme are :gold functions which can be executed and
which also have passed both the termination and the guard
verification proofs. The color of a function can be specified with
the new xargs keyword, :color, which, if omitted defaults to the
global setting of ld-color. Ld-color replaces load-mode. Setting
ld-color to :red causes behavior similar to the old :g-mode.
Setting ld-color to :gold causes behavior similar to the old
:v-mode. It is possible to prototype your system in :red and then
convert :red functions to :blue individually by calling
verify-termination on them. They can then be converted to :gold
with verify-guards. This allows us to undertake to verify the
termination and guards of system functions. See :doc color for an
introduction to the use of colors.
Type prescription rules have been added. Recall that in Nqthm, some
rewrite rules were actually stored as ``type-prescriptions.'' Such
rules allow the user to inform Nqthm's primitive type mechanism as
to the kinds of shells returned by a function. Earlier versions of
Acl2 did not have an analogous kind of rule because Acl2's type
mechanism is complicated by guards. Version 1.3 supports
type-prescription rules. See type-prescription.
Three more new rule-classes implement congruence-based rewriting.
It is possible to identify a binary relation as an equivalence
relation (see equivalence), to show that one equivalence
relation refines another (see refinement) and to show that a
given equivalence relation is maintained when rewriting a given
function call, e.g., (fn ...xk...), by maintaining another
equivalence relation while rewriting the kth argument
(see congruence). If r has been shown to be an equivalence
relation and then (implies hyps (r (foo x) (bar x))) is proved as a
:rewrite rule, then instances of (foo x) will be replaced by
corresponding instances of (bar x) provided the instance occurs in a
slot where the maintainence of r-equivalence is known to be
sufficient and hyps can be established as usual.
In Version 1.2, rule-classes were simple keywords, e.g., :rewrite or
:elim. In Version 1.3, rule-classes have been elaborated to allow
you to specify how the theorem ought to be used as a rule. That is,
the new rule-classes allows you to separate the mathematical
statement of the formula from its interpretation as a rule.
See rule-classes.
Rules used to be named by symbols, e.g., car and car-cons were the
names of rules. Unfortunately, this was ambiguous because there are
three rules associated with function symbols: the symbolic
definition, the executable counterpart, and the type-prescription;
many different rules might be associated with theorems, depending on
the rule classes. In Version 1.3 rules are named by ``runes''
(which is just short hand for ``rule names''). Example runes are
(:definition car), (:executable-counterpart car), and
(:type-prescription car . 1). Every rule added by an event has a
different name and you can enable and disable them independently.
See rune and see theories.
The identity function force, of one argument, has been added and
given a special interpretation by the functions responsible for
establishing hypotheses in backchaining: When the system fails to
establish some hypothesis of the form (force term), it simply
assumes it is true and goes on, delaying until later the
establishment of term. In particular, pushes a new subgoal to prove
term in the current context. When that subgoal is attacked, all of
the resources of the theorem prover, not just rewriting, are brought
to bear. Thus, for example, if you wish to prove the rule
(implies (good-statep s) (equal (exec s n) s')) and it is your
expectation that every time exec appears its first argument is a
good-statep then you might write the rule as
(implies (force (good-statep s)) (equal (exec s n) s')). This
rule is essentially an unconditional rewrite of (exec s n) to
s' that spawns the new goal (good-statep s). See force.
Because you can now specify independently how a theorem is used as a
rule, you need not write the force in the actual theorem proved.
See rule-classes.
Version 1.3 supports a facility similar to Nqthm's break-lemma.
See break-rewrite. You can install ``monitors'' on runes that
will cause interactive breaks under certain conditions.
Acl2 also provides ``wormholes'' which allow you to write functions
that cause interaction with the user but which do not require that
you have access to state. See wormhole.
The rewriter now automatically backchains to stronger recognizers.
There is no user hook to this feature but it may simplify some
proofs with which older versions of Acl2 had trouble. For example,
if the rewriter is trying to prove (rationalp (foo a b c)) it is now
smart enough to try lemmas that match with (integerp (foo a b c)).