Major Section: OTHER
Forms: (set-tainted-okp nil) ; do not allow incremental version mismatches (default) (set-tainted-okp t) ; allow incremental version mismatches
Set-tainted-okp is of use only in the presence of incremental releases.
In short, evaluation of
(set-tainted-okp t) instructs ACL2 to consider an
incremental release to have the same ACL2 version as the most recently
preceding normal release. BUT THIS IS NOT THE CASE BY DEFAULT BECAUSE ACL2
IS POTENTIALLY UNSOUND WHEN
SET-TAINTED-OKP IS EVALUATED.
Incremental releases have an incremental (incrl) version field, for
example the number 1 in version 2.9.1. (Also see version.) Ordinary
releases have an implicit incrl version field of 0 (for example, in version
2.9). By default,
certify-book consider all
fields of ACL2 version strings, including their incrl fields, in order to
decide if there are version mismatches. But it may be convenient to treat an
incremental release as the same as the corresponding (immediately preceding)
normal release, in order to avoid recertification of existing certified
books. SUCH RECERTIFICATION IS LOGICALLY REQUIRED, but we provide
(set-tainted-okp t) as a mechanism to allow users to experiment with
Below we describe how books can be certified even though their certification has depended on ignoring mismatches of incrl version fields. We call such certified books ``tainted''.
(set-tainted-okp t) is evaluated, then any discrepancy is ignored
between the incrl version field of an included book (representing the version
of ACL2 in which that book was certified) and the current ACL2 version,
namely the value of
(@ acl2-version). Thus, with
we allow certification of books that depend on included books that have such
version mismatches with the current ACL2 version or are themselves tainted.
Any book thus certified will have the string "(tainted)" included in its
certificate's version string. Indeed, when ACL2 detects that a
book may depend either on a book whose version's incrl field differs from
that of the current ACL2 version, or on a tainted book, then such a book
is marked as tainted.
(set-tainted-okp t) has been executed, then even though ACL2
``ignores'' issues of tainting as discussed above, a
is printed whenever a tainted book is included or certified.