Major Section: MISCELLANEOUS

To determine the version number of your copy of ACL2, evaluate the ACL2
constant `*acl2-version*`

. The value will be a string. For example,

ACL2 !>*acl2-version* "ACL2 Version 1.9"

Books are considered certified only in the same version of ACL2 in which the certification was done. The certificate file records the version number of the certifying ACL2 and include-book considers the book uncertified if that does not match the current version number. Thus, each time we release a new version of ACL2, previously certified books should be recertified.

One reason for this is immediately obvious from the fact that the version number is a logical constant in the ACL2 theory: changing the version number changes the axioms! For example, in version 1.8 you can prove

(defthm version-8 (equal *acl2-version* "ACL2 Version 1.8"))while in version 1.9 you can prove

(defthm version-9 (equal *acl2-version* "ACL2 Version 1.9"))Thus, if a book containing the former were included into version 1.9, one could prove a contradiction.

We could eliminate this particular threat of unsoundness by not
making the version number part of the axioms. But there are over
150 constants in the system, most having to do with the fact that
ACL2 is coded in ACL2, and ``version number inconsistency'' is just
the tip of the iceberg. Other likely-to-change constants include
`*common-lisp-specials-and-constants*`

, which may change when we
port ACL2 to some new implementation of Common Lisp, and
`*acl2-exports*`

, which lists commonly used ACL2 command names
users are likely to import into new packages. Furthermore, it is
possible that from one version of the system to another we might
change, say, the default values on some system function or otherwise
make ``intentional'' changes to the axioms. It is even possible one
version of the system is discovered to be unsound and we release a
new version to correct our error.

Therefore we adopted the draconian policy that books are certified
by a given version of ACL2 and ``must'' be recertified to be used
in other versions. We put ``must'' in quotes because in fact, ACL2
allows a book that was certified in one ACL2 version to be included
in a later version, using `include-book`

. But ACL2 does not allow
`certify-book`

to succeed when such an `include-book`

is executed on its
behalf. Also, you may experience undesirable behavior if you avoid
recertification when moving to a different version. (We try to
prevent some undesirable behavior by refusing to load the compiled
code for an uncertified book, but this does not guarantee good
behavior.) Hence we recommend that you stick to the draconion
policy of recertifying books when updating to a new ACL2 version.

The string `*acl2-version*`

can contain implementation-specific
information in addition to the version number. For example, in
Macintosh Common Lisp (MCL) `(char-code #Newline)`

is 13, while as
far as we know, it is 10 in every other Common Lisp. Our concern is
that one could certify a book in an MCL-based ACL2 with the theorem

(equal (char-code #Newline) 13)and then include this book in another Lisp and thereby prove

`nil`

.
So, when a book is certified in an MCL-based ACL2, the book's
certificate mentions ``MCL'' in its version string. Moreover,
`*acl2-version*`

similarly mentions ``MCL'' when the ACL2 image has
been built on top of MCL. Thus, an attempt to include a book in an
MCL-based ACL2 that was certified in a non-MCL-based ACL2, or
vice-versa, will be treated like an attempt to include an
uncertified book.