|
|
|---|
|
|
|
|---|
Deeming a book uncertified because of a book-hash mismatch
When include-book is invoked, the specified book may be considered uncertified by ACL2 because its book-hash — which by default is an alist specifying the book's size and write-date, but could be a checksum — does not match what was expected. In that case you will typically see a warning such as the following, which instead will be an error if this occurs during certification. In this topic, we explain how this warning can occur.
ACL2 Warning [Uncertified] in ( INCLUDE-BOOK "foo" ...): The certificate for "/Users/kaufmann/temp/foo.lisp" lists the book- hash of that book as ((:BOOK-LENGTH . 38) (:BOOK-WRITE-DATE . 3674050905)). But its book-hash is now computed to be ((:BOOK-LENGTH . 39) (:BOOK-WRITE-DATE . 3674050914)). See :DOC book-hash-mismatch.
Probably the simplest way for such a mismatch to occur is if you change the
book after certifying it, and then try to include the book. In the example
message displayed above, the book-hash for
The mismatch might occur on a book that is being included while including a
superior book. For example, suppose that the act of evaluating
There are several ways for a book-hash in a
Note that it is possible to mix alist and checksum book-hash values. The
key is to avoid conflicts between book-hash values stored for the same book in
different
(certify-book "sub") (u) (assign book-hash-alistp t) (certify-book "top") ; contains the event (include-book "sub") (u) (include-book "top") ; no problem!
However, if we instead evaluate the following forms in a fresh ACL2
session, the last one causes an error, because a checksum serves as the
book-hash for
(certify-book "sub") :u (certify-book "top") ; contains the event (include-book "sub") :u (assign book-hash-alistp t) (certify-book "sub") ; now the book-hash for sub is an alist :u ; Error: mismatch for book-hash values for "sub" in ; new sub.cert and earlier top.cert. (include-book "top")
That said, ACL2 does not care about the current value of state global
(assign book-hash-alistp nil) (certify-book "foo") (assign book-hash-alistp t) (include-book "foo")
We conclude by discussing a rather insidious book-hash mismatch that can
occur when including a book using an ACL2 executable that differs from the
executable that was used when certifying the book. Here is an example.
Consider a book,
ACL2 Warning [Uncertified] in ( INCLUDE-BOOK "foo" ...): After including the book "/Users/smith/temp/foo.lisp": -- its certificate requires the book "/Users/smith/acl2/books/tools/remove- hyps.lisp" with certificate annotations ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) and book hash 1958615726, but we have included a version of "remove-hyps" with certificate annotations ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) and book-hash ((:BOOK-LENGTH . 14650) (:BOOK-WRITE-DATE . 3656629263)), so book recertification is probably required;