Major Section: MISCELLANEOUS
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 3.1"
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.
