		Search-engine friendly clone of the ACL2 documentation.

About-ACL2

Version

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 3.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 documentation 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. Hence we recommend that you stick to the draconion policy of recertifying books when updating to a new ACL2 version.

Furthermore, all bets are off if you certify a book using ACL2 built on one host Lisp implementation and include the book using ACL2 built on a different host Lisp implementation. For example, for most host Lisp implementations, the Lisp reader will interpret the token 2f as a symbol; however, Common Lisp allows for the possibility that 2f is read as a number. In such a case, one could use the former ACL2 executable to certify a book containing the form

(defthm my-thm
  (symbolp '2f)
  :rule-classes nil)

but then use the latter ACL2 executable to include the book, even though for the latter ACL2 executable, 2f is a number, not a symbol. Of course, one would expect an error because of a book-hash mismatch) in such case. But these do not provide guaranteed protection against including uncertified books.

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 incremental releases are full-fledged releases.