VERSION

ACL2 Version Number 
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.