ACL2 Version 2.0 (July, 1997) Notes
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.


ACL2 Version 2.1 (December, 1997) Notes
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.


ACL2 Version 2.2 (August, 1998) Notes
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.


ACL2 Version 2.3 (October, 1998) Notes
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.


ACL2 Version 2.4 (August, 1999) Notes
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.


ACL2 Version 2.5 (June, 2000) Notes
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).

(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-cbd may now take a relative pathname as an argument.

(3) When the macro ld is given a file name as a value for standard-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 the ld specials standard-co and proofs-co.

It is no longer necessary to issue :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.


Acl2 Version 1.1 Notes
Major Section:  RELEASE-NOTES

The new features are extensively documented. The relevant topics are:

It is especially important to read all of of the documentation for books before trying to use books. However, the new :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.


Acl2 Version 1.2 Notes
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.


Acl2 Version 1.3 Notes
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)).