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