SET-TAINTED-OKP

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, include-book and 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 incremental releases.

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''.

If (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 (set-tainted-okp t) 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.

When (set-tainted-okp t) has been executed, then even though ACL2 ``ignores'' issues of tainting as discussed above, a "Tainted" warning is printed whenever a tainted book is included or certified.