ACL2 Version Number

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"


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.



(equal (char-code #Newline) 13)