acl2 - cert.pl が ttag について不平を言うのはなぜですか

Question

ACL2 書籍の認定時に、次のエラー メッセージが表示されることがよくあります。

| ACL2 Error in ( INCLUDE-BOOK "something" ...):  The ttag :FAST-CAT
| associated with file /elided/acl2/books/std/string\
| s/fast-cat.lisp is not among the set of ttags permitted in the current
| context, specified as follows:
|   NIL.
| See :DOC defttag.

どうしたの？

Answer 1

証明しようとしている本を含むディレクトリにファイルを追加する必要があり<something>.acl2ます (通常は問題なく動作します)。cert.acl2このファイルは、たとえば次のコードを使用して、使用してもよい<something>.acl2ことを指示する必要があります。cert.plttags

(in-package "ACL2")

; cert-flags: ? t :ttags :all