ACL2 Version Number

To determine the version number of your copy of ACL2, evaluate the form (@ acl2-version). The value will be a string. For example,

ACL2 !>(@ acl2-version)
"ACL2 Version 2.9.4"

The part of the string after "ACL2 Version " is of the form x.y or x.y.z, optionally followed by a succession of values in parentheses, where x, y, and z are natural numbers. If z is omitted then it is implicitly 0. We refer to X, y, and z as the ``major'', ``minor'', and ``incrl'' fields, respectively. The incrl field is used for incremental releases. The discussion just below assumes that incremental releases are not employed at the user's site, i.e., the incrl fields are always 0. We remove this assumption when we discuss incremental releases at the end of this documenttation topic.

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.

Note that there are over 150 constants in the system, most having to do with the fact that ACL2 is coded in ACL2. Many of these, for example *common-lisp-specials-and-constants* and *acl2-exports*, may change from version to version, and this can cause unsoundness. For example, the symbol 'set-difference-eq was added to *acl2-exports* in Version_2.9, so we can certify a book in Version_2.8 containing the following theorem, which is false in Version_2.9.

(null (member 'set-difference-eq *acl2-exports*))
Therefore, we need to disallow inclusion of such a book in a Version_2.9 session, which otherwise would allow us to prove nil. 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.

Incremental releases.

From time to time, so-called ``incremental releases'' of ACL2 are made available. These releases are thoroughly tested on at least two platforms; ``normal'' releases, on the other hand, are thoroughly tested on many more platforms (perhaps a dozen or so) and are accompanied by updates to the ACL2 home page. We provide incremental releases in order to provide timely updates for ACL2 users who want them, without imposing unnecessary burdens on either on the ACL2 implementors or on ACL2 users who prefer to update less frequently. The implementors expect users to update their copies of ACL2 when normal releases are made available, but not necessarily when incremental releases are made available.

Incremental releases are accompanied by a bump in the incrl field of the version field, while normal releases are accompanied by a bump in the minor or (much less frequently) major field and zeroing out of the incrl field.

Note that LOGICALLY SPEAKING, INCREMENTAL RELEASES ARE FULL-FLEDGE RELEASES. However, ACL2 users may wish to experiment with incremental releases without recertifying all of their existing ACL2 books (see certify-book). In order to learn how to avoid such recertification, see set-tainted-okp. The basic idea is that if certification may depend on including books from an ACL2 version with a different incrl field, the book's certificate is marked with a ``tainted'' version, i.e., a version with "(tainted" as a substring. Subsequent inclusion of any such book is restricted to sessions in which the user explicitly invokes (set-tainted-okp t), which is intended as an acknowledgment that including such a book may render the ACL2 session unsound.