ACL2 Version Number
To determine the version number of your copy of ACL2, evaluate the
ACL2 !>(@ acl2-version) "ACL2 Version 3.4"
The part of the string after
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
(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
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
(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,
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.